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

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 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 y : M) : f (x + y) = f x + f y + polar f x y

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

theorem QuadraticMap.polar_neg {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : M → N) (x y : M) : polar (-f) x y = -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 y : M) : polar (s • f) x y = s • polar f x y

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

def QuadraticMap.polarSym2 {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : M → N) : Sym2 M → N

QuadraticMap.polar as a function from Sym2.

Equations

• QuadraticMap.polarSym2 f = Sym2.lift ⟨QuadraticMap.polar f, ⋯⟩

@[simp]

theorem QuadraticMap.polarSym2_sym2Mk {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : M → N) (xy : M × M) : polarSym2 f (Sym2.mk xy) = polar f xy.1 xy.2

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

  The underlying function.

  Do NOT use directly. Use the coercion instead.

• 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

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

@[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.

@[simp]

theorem QuadraticMap.coe_mk {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x) (exists_companion' : ∃ (B : LinearMap.BilinMap R M N), ∀ (x y : M), toFun (x + y) = toFun x + toFun y + (B x) y) : ⇑{ toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' } = 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 Q' : QuadraticMap R M N} (H : ∀ (x : M), Q x = Q' x) : Q = Q'

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 Q' : QuadraticMap R M N} : Q = Q' ↔ ∀ (x : M), Q x = Q' x

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 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} [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 y 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

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] [SMul 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 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) : 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 x' y : M) : polar (⇑Q) (x + x') y = polar (⇑Q) x y + 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 y : M) : polar (⇑Q) (a • x) y = a • 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 y : M) : polar (⇑Q) (-x) y = -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 x' y : M) : polar (⇑Q) (x - x') y = polar (⇑Q) x y - 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) : 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 y y' : M) : polar (⇑Q) x (y + y') = polar (⇑Q) x y + 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 y : M) : polar (⇑Q) x (a • y) = a • 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 y : M) : polar (⇑Q) x (-y) = -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 y y' : M) : polar (⇑Q) x (y - y') = polar (⇑Q) x y - 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) : polar (⇑Q) x x = 2 • Q x

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.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 y : M) : (Q.polarBilin m) y = polar (⇑Q) m y

theorem QuadraticMap.polarSym2_map_smul {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) (g : ι → M) (l : ι → R) (p : Sym2 ι) : polarSym2 (⇑Q) (Sym2.map (l • g) p) = (Sym2.map l p).mul • polarSym2 (⇑Q) (Sym2.map g p)

@[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 y : M) : polar (⇑Q) (a • x) y = a • 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 y : M) : polar (⇑Q) x (a • y) = a • polar (⇑Q) x y

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), polar toFun (x + x') y = polar toFun x y + polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • 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' := ⋯ }

@[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), polar toFun (x + x') y = polar toFun x y + polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y) (a✝ : M) : (ofPolar toFun toFun_smul polar_add_left polar_smul_left) a✝ = toFun a✝

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 ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f 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, polarSym2 (⇑Q) (Sym2.map f 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)

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)

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 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 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) ⋯ ⋯ ⋯ ⋯

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.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 : M) : coeFnAddMonoidHom a✝ a = a✝ a

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.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) : (evalAddMonoidHom m) a✝ = a✝ m

@[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 = { toSMul := QuadraticMap.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

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 = { toDistribMulAction := QuadraticMap.instDistribMulActionOfSMulCommClass, add_smul := ⋯, zero_smul := ⋯ }

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 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 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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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 Q : M → N is a quadratic map of R-modules and R is an S-algebra, then the restriction of scalars is a quadratic map of S-modules.

Equations

• Q.restrictScalars = { toFun := fun (x : M) => Q x, toFun_smul := ⋯, exists_companion' := ⋯ }

@[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.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)

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 {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' {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

@[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 LinearEquiv.congrQuadraticMap {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] (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P

When N and P are equivalent, quadratic maps on M into N are equivalent to quadratic maps on M into P.

See LinearMap.BilinMap.congr₂ for the bilinear map version.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.congrQuadraticMap_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] (e : N ≃ₗ[R] P) (Q : QuadraticMap R M N) : e.congrQuadraticMap Q = (↑e).compQuadraticMap Q

@[simp]

theorem LinearEquiv.congrQuadraticMap_symm_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] (e : N ≃ₗ[R] P) (Q : QuadraticMap R M P) : e.congrQuadraticMap.symm Q = (↑e.symm).compQuadraticMap Q

@[simp]

theorem LinearEquiv.congrQuadraticMap_refl {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : (refl R N).congrQuadraticMap = refl R (QuadraticMap R M N)

@[simp]

theorem LinearEquiv.congrQuadraticMap_symm {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] (e : N ≃ₗ[R] P) : e.congrQuadraticMap.symm = e.symm.congrQuadraticMap

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 g : M →ₗ[R] A) : QuadraticMap R M A

The product of linear maps into an R-algebra is a quadratic map.

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 g : M →ₗ[R] A) (x : M) : (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 g h : M →ₗ[R] A) : linMulLin (f + g) h = linMulLin f h + 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 g h : M →ₗ[R] A) : linMulLin f (g + h) = linMulLin f g + 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 g : M →ₗ[R] A) (h : N' →ₗ[R] M) : (linMulLin f g).comp h = linMulLin (f ∘ₗ h) (g ∘ₗ h)

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 map sending the vector x : A to x * x

Equations

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

@[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) : sq a = a * a

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 j : n) : QuadraticMap R (n → A) A

proj i j is the quadratic map sending 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 j : n) (x : n → A) : (proj i j) x = x i * x j

Associated bilinear maps

If multiplication by 2 is invertible on the target module N of QuadraticMap R M N, then there is a linear bijection QuadraticMap.associated between quadratic maps Q over R from M to N and symmetric bilinear maps B : M →ₗ[R] M →ₗ[R] → N such that BilinMap.toQuadraticMap B = Q (see QuadraticMap.associated_rightInverse). The associated bilinear map is half Q.polarBilin (see QuadraticMap.two_nsmul_associated); this is where the invertibility condition comes from. We spell the condition as [Invertible (2 : Module.End R N)].

Note that this makes the bijection available in more cases than the simpler condition Invertible (2 : R), e.g., when R = ℤ and N = ℝ.

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) : toQuadraticMap (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] : 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₁ 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

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.BilinMap.toQuadraticMap as an additive homomorphism

Equations

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

@[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) : (toQuadraticMapAddMonoidHom R M) B = B.toQuadraticMap

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.BilinMap.toQuadraticMap as a linear map

Equations

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

@[simp]

theorem LinearMap.BilinMap.toQuadraticMapLinearMap_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) : (toQuadraticMapLinearMap S R M) B = B.toQuadraticMap

@[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 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 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 ↔ 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₁ 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 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 + 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 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 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 = compr₂ Q.polarBilin f

instance QuadraticMap.instSMulCommClassSubtypeMemSubmonoidCenter {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : SMulCommClass R (↥(Submonoid.center R)) M

instance QuadraticMap.instInvertibleEndOfNat {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Invertible 2] : Invertible 2

If 2 is invertible in R, then it is also invertible in End R M.

Equations

• QuadraticMap.instInvertibleEndOfNat = { invOf := ⟨⅟2, ⋯⟩ • 1, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

theorem QuadraticMap.half_moduleEnd_apply_eq_half_smul {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Invertible 2] (x : M) : ⅟2 x = ⅟2 • x

If 2 is invertible in R, then applying the inverse of 2 in End R M to an element of M is the same as multiplying by the inverse of 2 in R.

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 ring and R is an S-algebra.

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 = { toFun := fun (Q : QuadraticMap R M N) => ⅟2 • Q.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 y : M) : (((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 • (associatedHom S) Q = Q.polarBilin

Twice the associated bilinear map of Q is the same as the polar of Q.

theorem QuadraticMap.associated_isSymm (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 y : M) : (((associatedHom S) Q) x) y = (((associatedHom S) Q) y) x

theorem QuadraticForm.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] (Q : QuadraticForm R M) [Invertible 2] : LinearMap.IsSymm ((QuadraticMap.associatedHom S) Q)

theorem QuadraticMap.associated_flip (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) : LinearMap.flip ((associatedHom S) Q) = (associatedHom S) Q

A version of QuadraticMap.associated_isSymm for general targets (using flip because IsSymm does not apply here).

@[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) : (associatedHom S) (Q.comp f) = LinearMap.compl₁₂ ((associatedHom S) Q) f f

theorem QuadraticMap.associated_toQuadraticMap (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] (B : LinearMap.BilinMap R M N) (x y : M) : (((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} {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] {B₁ : LinearMap.BilinMap R M N} (h : ∀ (x y : M), (B₁ x) y = (B₁ y) x) : (associatedHom S) B₁.toQuadraticMap = B₁

theorem QuadraticMap.associated_left_inverse' (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] {B₁ : LinearMap.BilinMap R M N} (hB₁ : LinearMap.flip B₁ = B₁) : (associatedHom S) B₁.toQuadraticMap = B₁

A version of QuadraticMap.associated_left_inverse for general targets.

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) : (((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) : ((associatedHom S) Q).toQuadraticMap = Q

theorem QuadraticMap.associated_rightInverse (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] : Function.RightInverse (⇑(associatedHom S)) LinearMap.BilinMap.toQuadraticMap

@[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 →ₗ[ℤ] LinearMap.BilinMap R M N

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) (⇑(associatedHom ℕ)) LinearMap.IsSymm

Symmetric bilinear forms can be lifted to quadratic forms

instance QuadraticMap.canLift' {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] : CanLift (LinearMap.BilinMap R M N) (QuadraticMap R M N) ⇑(associatedHom ℕ) fun (B : LinearMap.BilinMap R M N) => LinearMap.flip B = B

Symmetric bilinear maps can be lifted to quadratic maps

theorem QuadraticMap.exists_quadraticMap_ne_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] [Invertible 2] {Q : QuadraticMap R M N} (hB₁ : 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] : ⇑(associatedHom S) = ⇑associated

@[simp]

theorem QuadraticMap.associated_linMulLin {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (f g : M →ₗ[R] R) : associated (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] : associated 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 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 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 y : M) : 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 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 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 y : M} (h : IsSymm B) : B.toQuadraticMap.IsOrtho x y ↔ 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 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 y : M} (h : Q.IsOrtho x y) : 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 y : M} : LinearMap.IsOrtho (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 (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} [CommSemiring R] [PartialOrder 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] [AddLeftStrictMono N] (Q 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} [CommSemiring R] [Module R M] [Semiring A] [LinearOrder A] [IsStrictOrderedRing A] [ExistsAddOfLE A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) (hf : LinearMap.ker f = ⊥) : (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 : QuadraticForm R (n → R)) : (toMatrix' Q).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 : (BilinMap.toQuadraticMap B).Anisotropic) : 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₂ : IsSymm B) : ∃ (x : M), ¬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₂ : IsSymm B) : ∃ (v : Module.Basis (Fin (Module.finrank K V)) K V), 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 : Module.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 : Module.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) : (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 : QuadraticForm R M) (v : Module.Basis ι R M) (hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v) : basisRepr Q v = weightedSumSquares R fun (i : ι) => Q (v i)

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