Quadratic forms

This file defines quadratic forms over a R-module M. A quadratic form on a commutative ring R is a map Q : M → R such that:

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

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

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

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

Main definitions

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

Main statements

• QuadraticForm.associated_left_inverse,
• QuadraticForm.associated_rightInverse: in a commutative ring where 2 has an inverse, there is a correspondence between quadratic forms and symmetric bilinear forms
• LinearMap.BilinForm.exists_orthogonal_basis: There exists an orthogonal basis with respect to any nondegenerate, symmetric bilinear form 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 form in the noncommutative setting would require substantial refactors from the current version, such that $Q(rm) = rQ(m)r^$forsomesuitableconjugation$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 form, homogeneous polynomial, quadratic polynomial

def QuadraticForm.polar {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] (f : M → R) (x : M) (y : M) : R

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

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

Equations

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

theorem QuadraticForm.polar_add {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] (f : M → R) (g : M → R) (x : M) (y : M) : QuadraticForm.polar (f + g) x y = QuadraticForm.polar f x y + QuadraticForm.polar g x y

theorem QuadraticForm.polar_neg {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] (f : M → R) (x : M) (y : M) : QuadraticForm.polar (-f) x y = -QuadraticForm.polar f x y

theorem QuadraticForm.polar_smul {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Monoid S] [DistribMulAction S R] (f : M → R) (s : S) (x : M) (y : M) : QuadraticForm.polar (s • f) x y = s • QuadraticForm.polar f x y

theorem QuadraticForm.polar_comm {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] (f : M → R) (x : M) (y : M) : QuadraticForm.polar f x y = QuadraticForm.polar f y x

theorem QuadraticForm.polar_add_left_iff {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] {f : M → R} {x : M} {x' : M} {y : M} : QuadraticForm.polar f (x + x') y = QuadraticForm.polar f x y + QuadraticForm.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 QuadraticForm.polar without subtraction.

theorem QuadraticForm.polar_comp {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] {F : Type u_6} [CommRing S] [FunLike F R S] [AddMonoidHomClass F R S] (f : M → R) (g : F) (x : M) (y : M) : QuadraticForm.polar (⇑g ∘ f) x y = g (QuadraticForm.polar f x y)

structure QuadraticForm (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max u v)

A quadratic form over a module.

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

• toFun : M → R
• toFun_smul : ∀ (a : R) (x : M), self.toFun (a • x) = a * a * self.toFun x
• exists_companion' : ∃ (B : LinearMap.BilinForm R M), ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B x) y

Instances For

• QuadraticForm.canLift
• QuadraticForm.instAdd
• QuadraticForm.instAddCommGroup
• QuadraticForm.instAddCommMonoid
• QuadraticForm.instCoeFunForall
• QuadraticForm.instDistribMulActionOfSMulCommClass
• QuadraticForm.instFunLike
• QuadraticForm.instInhabited
• QuadraticForm.instIsScalarTower
• QuadraticForm.instModuleOfSMulCommClass
• QuadraticForm.instNeg
• QuadraticForm.instSMul
• QuadraticForm.instSMulCommClass
• QuadraticForm.instSub
• QuadraticForm.instZero
• QuadraticForm.zeroHomClass

theorem QuadraticForm.toFun_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (self : QuadraticForm R M) (a : R) (x : M) : self.toFun (a • x) = a * a * self.toFun x

theorem QuadraticForm.exists_companion' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (self : QuadraticForm R M) : ∃ (B : LinearMap.BilinForm R M), ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B x) y

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

Equations

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

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

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

Equations

• QuadraticForm.instCoeFunForall = { coe := DFunLike.coe }

@[simp]

theorem QuadraticForm.toFun_eq_coe {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : Q.toFun = ⇑Q

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

theorem QuadraticForm.ext {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} (H : ∀ (x : M), Q x = Q' x) : Q = Q'

theorem QuadraticForm.congr_fun {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} (h : Q = Q') (x : M) : Q x = Q' x

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

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

Copy of a QuadraticForm 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 QuadraticForm.coe_copy {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (Q' : M → R) (h : Q' = ⇑Q) : ⇑(Q.copy Q' h) = Q'

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

theorem QuadraticForm.map_smul {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (a : R) (x : M) : Q (a • x) = a * a * Q x

theorem QuadraticForm.exists_companion {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : ∃ (B : LinearMap.BilinForm R M), ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y

theorem QuadraticForm.map_add_add_add_map {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (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 QuadraticForm.map_add_self {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (x : M) : Q (x + x) = 4 * Q x

theorem QuadraticForm.map_zero {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : Q 0 = 0

instance QuadraticForm.zeroHomClass {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] : ZeroHomClass (QuadraticForm R M) M R

Equations

• ⋯ = ⋯

theorem QuadraticForm.map_smul_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (a : S) (x : M) : Q (a • x) = (a * a) • Q x

@[simp]

theorem QuadraticForm.map_neg {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) : Q (-x) = Q x

theorem QuadraticForm.map_sub {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) (y : M) : Q (x - y) = Q (y - x)

@[simp]

theorem QuadraticForm.polar_zero_left {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (y : M) : QuadraticForm.polar (⇑Q) 0 y = 0

@[simp]

theorem QuadraticForm.polar_add_left {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) (x' : M) (y : M) : QuadraticForm.polar (⇑Q) (x + x') y = QuadraticForm.polar (⇑Q) x y + QuadraticForm.polar (⇑Q) x' y

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuadraticForm.polar_zero_right {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (y : M) : QuadraticForm.polar (⇑Q) y 0 = 0

@[simp]

theorem QuadraticForm.polar_add_right {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) (y : M) (y' : M) : QuadraticForm.polar (⇑Q) x (y + y') = QuadraticForm.polar (⇑Q) x y + QuadraticForm.polar (⇑Q) x y'

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuadraticForm.polar_self {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) : QuadraticForm.polar (⇑Q) x x = 2 * Q x

@[simp]

theorem QuadraticForm.polarBilin_apply_apply {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) (y : M) : (Q.polarBilin m) y = QuadraticForm.polar (⇑Q) m y

def QuadraticForm.polarBilin {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : LinearMap.BilinForm R M

QuadraticForm.polar as a bilinear map

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuadraticForm.ofPolar_apply {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (toFun : M → R) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = a * a * toFun x) (polar_add_left : ∀ (x x' y : M), QuadraticForm.polar toFun (x + x') y = QuadraticForm.polar toFun x y + QuadraticForm.polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), QuadraticForm.polar toFun (a • x) y = a • QuadraticForm.polar toFun x y) : ∀ (a : M), (QuadraticForm.ofPolar toFun toFun_smul polar_add_left polar_smul_left) a = toFun a

def QuadraticForm.ofPolar {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (toFun : M → R) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = a * a * toFun x) (polar_add_left : ∀ (x x' y : M), QuadraticForm.polar toFun (x + x') y = QuadraticForm.polar toFun x y + QuadraticForm.polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), QuadraticForm.polar toFun (a • x) y = a • QuadraticForm.polar toFun x y) : QuadraticForm R M

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

Equations

• QuadraticForm.ofPolar toFun toFun_smul polar_add_left polar_smul_left = { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := ⋯ }

theorem QuadraticForm.choose_exists_companion {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ⋯.choose = Q.polarBilin

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

instance QuadraticForm.instSMul {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] : SMul S (QuadraticForm R M)

QuadraticForm R M inherits the scalar action from any algebra over R.

This provides an R-action via Algebra.id.

Equations

• QuadraticForm.instSMul = { smul := fun (a : S) (Q : QuadraticForm R M) => { toFun := a • ⇑Q, toFun_smul := ⋯, exists_companion' := ⋯ } }

@[simp]

theorem QuadraticForm.coeFn_smul {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (a : S) (Q : QuadraticForm R M) : ⇑(a • Q) = a • ⇑Q

@[simp]

theorem QuadraticForm.smul_apply {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (a : S) (Q : QuadraticForm R M) (x : M) : (a • Q) x = a • Q x

instance QuadraticForm.instSMulCommClass {S : Type u_1} {T : Type u_2} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Monoid S] [Monoid T] [DistribMulAction S R] [DistribMulAction T R] [SMulCommClass S R R] [SMulCommClass T R R] [SMulCommClass S T R] : SMulCommClass S T (QuadraticForm R M)

Equations

• ⋯ = ⋯

instance QuadraticForm.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Monoid S] [Monoid T] [DistribMulAction S R] [DistribMulAction T R] [SMulCommClass S R R] [SMulCommClass T R R] [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticForm R M)

Equations

• ⋯ = ⋯

instance QuadraticForm.instZero {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] : Zero (QuadraticForm R M)

Equations

• QuadraticForm.instZero = { zero := { toFun := fun (x : M) => 0, toFun_smul := ⋯, exists_companion' := ⋯ } }

@[simp]

theorem QuadraticForm.coeFn_zero {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] : ⇑0 = 0

@[simp]

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

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

Equations

• QuadraticForm.instInhabited = { default := 0 }

instance QuadraticForm.instAdd {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] : Add (QuadraticForm R M)

Equations

• QuadraticForm.instAdd = { add := fun (Q Q' : QuadraticForm R M) => { toFun := ⇑Q + ⇑Q', toFun_smul := ⋯, exists_companion' := ⋯ } }

@[simp]

theorem QuadraticForm.coeFn_add {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) : ⇑(Q + Q') = ⇑Q + ⇑Q'

@[simp]

theorem QuadraticForm.add_apply {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (x : M) : (Q + Q') x = Q x + Q' x

instance QuadraticForm.instAddCommMonoid {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] : AddCommMonoid (QuadraticForm R M)

Equations

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

@[simp]

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

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

@CoeFn (QuadraticForm R M) as an AddMonoidHom.

This API mirrors AddMonoidHom.coeFn.

Equations

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

@[simp]

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

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

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

Equations

• QuadraticForm.evalAddMonoidHom m = (Pi.evalAddMonoidHom (fun (a : M) => R) m).comp QuadraticForm.coeFnAddMonoidHom

@[simp]

theorem QuadraticForm.coeFn_sum {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} (Q : ι → QuadraticForm R M) (s : Finset ι) : ⇑(s.sum fun (i : ι) => Q i) = s.sum fun (i : ι) => ⇑(Q i)

@[simp]

theorem QuadraticForm.sum_apply {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} (Q : ι → QuadraticForm R M) (s : Finset ι) (x : M) : (s.sum fun (i : ι) => Q i) x = s.sum fun (i : ι) => (Q i) x

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

Equations

• QuadraticForm.instDistribMulActionOfSMulCommClass = DistribMulAction.mk ⋯ ⋯

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

Equations

• QuadraticForm.instModuleOfSMulCommClass = Module.mk ⋯ ⋯

instance QuadraticForm.instNeg {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] : Neg (QuadraticForm R M)

Equations

• QuadraticForm.instNeg = { neg := fun (Q : QuadraticForm R M) => { toFun := -⇑Q, toFun_smul := ⋯, exists_companion' := ⋯ } }

@[simp]

theorem QuadraticForm.coeFn_neg {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ⇑(-Q) = -⇑Q

@[simp]

theorem QuadraticForm.neg_apply {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) : (-Q) x = -Q x

instance QuadraticForm.instSub {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] : Sub (QuadraticForm R M)

Equations

• QuadraticForm.instSub = { sub := fun (Q Q' : QuadraticForm R M) => (Q + -Q').copy (⇑Q - ⇑Q') ⋯ }

@[simp]

theorem QuadraticForm.coeFn_sub {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) : ⇑(Q - Q') = ⇑Q - ⇑Q'

@[simp]

theorem QuadraticForm.sub_apply {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (x : M) : (Q - Q') x = Q x - Q' x

instance QuadraticForm.instAddCommGroup {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] : AddCommGroup (QuadraticForm R M)

Equations

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

def QuadraticForm.comp {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 : QuadraticForm R N) (f : M →ₗ[R] N) : QuadraticForm R M

Compose the quadratic form with a linear function.

Equations

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

@[simp]

theorem QuadraticForm.comp_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 : QuadraticForm R N) (f : M →ₗ[R] N) (x : M) : (Q.comp f) x = Q (f x)

@[simp]

theorem LinearMap.compQuadraticForm_apply {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (f : R →ₗ[S] S) (Q : QuadraticForm R M) (x : M) : (f.compQuadraticForm Q) x = f (Q x)

def LinearMap.compQuadraticForm {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (f : R →ₗ[S] S) (Q : QuadraticForm R M) : QuadraticForm S M

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

Equations

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

def QuadraticForm.linMulLin {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) (g : M →ₗ[R] R) : QuadraticForm R M

The product of linear forms is a quadratic form.

Equations

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

@[simp]

theorem QuadraticForm.linMulLin_apply {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) (g : M →ₗ[R] R) (x : M) : (QuadraticForm.linMulLin f g) x = f x * g x

@[simp]

theorem QuadraticForm.add_linMulLin {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) (g : M →ₗ[R] R) (h : M →ₗ[R] R) : QuadraticForm.linMulLin (f + g) h = QuadraticForm.linMulLin f h + QuadraticForm.linMulLin g h

@[simp]

theorem QuadraticForm.linMulLin_add {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) (g : M →ₗ[R] R) (h : M →ₗ[R] R) : QuadraticForm.linMulLin f (g + h) = QuadraticForm.linMulLin f g + QuadraticForm.linMulLin f h

@[simp]

theorem QuadraticForm.linMulLin_comp {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] R) (g : M →ₗ[R] R) (h : N →ₗ[R] M) : (QuadraticForm.linMulLin f g).comp h = QuadraticForm.linMulLin (f ∘ₗ h) (g ∘ₗ h)

@[simp]

theorem QuadraticForm.sq_apply {R : Type u_3} [CommSemiring R] (a : R) : QuadraticForm.sq a = a * a

def QuadraticForm.sq {R : Type u_3} [CommSemiring R] : QuadraticForm R R

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

Equations

• QuadraticForm.sq = QuadraticForm.linMulLin LinearMap.id LinearMap.id

def QuadraticForm.proj {R : Type u_3} [CommSemiring R] {n : Type u_6} (i : n) (j : n) : QuadraticForm R (n → R)

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

Equations

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

@[simp]

theorem QuadraticForm.proj_apply {R : Type u_3} [CommSemiring R] {n : Type u_6} (i : n) (j : n) (x : n → R) : (QuadraticForm.proj i j) x = x i * x j

Associated bilinear forms

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

def LinearMap.BilinForm.toQuadraticForm {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : QuadraticForm R M

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

Equations

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

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_apply {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (x : M) : B.toQuadraticForm x = (B x) x

theorem LinearMap.BilinForm.toQuadraticForm_comp_same {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (B : LinearMap.BilinForm R N) (f : M →ₗ[R] N) : LinearMap.BilinForm.toQuadraticForm (LinearMap.compl₁₂ B f f) = B.toQuadraticForm.comp f

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_zero (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm.toQuadraticForm 0 = 0

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_add {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (B₁ : LinearMap.BilinForm R M) (B₂ : LinearMap.BilinForm R M) : (B₁ + B₂).toQuadraticForm = B₁.toQuadraticForm + B₂.toQuadraticForm

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_smul {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (a : S) (B : LinearMap.BilinForm R M) : (a • B).toQuadraticForm = a • B.toQuadraticForm

@[simp]

theorem LinearMap.BilinForm.toQuadraticFormAddMonoidHom_apply (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : (LinearMap.BilinForm.toQuadraticFormAddMonoidHom R M) B = B.toQuadraticForm

def LinearMap.BilinForm.toQuadraticFormAddMonoidHom (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm R M →+ QuadraticForm R M

LinearMap.BilinForm.toQuadraticForm as an additive homomorphism

Equations

• LinearMap.BilinForm.toQuadraticFormAddMonoidHom R M = { toFun := LinearMap.BilinForm.toQuadraticForm, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearMap.BilinForm.toQuadraticFormLinearMap_apply_apply (S : Type u_1) (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S R] [SMulCommClass S R R] [SMulCommClass R S R] (B : LinearMap.BilinForm R M) (x : M) : ((LinearMap.BilinForm.toQuadraticFormLinearMap S R M) B) x = (B x) x

def LinearMap.BilinForm.toQuadraticFormLinearMap (S : Type u_1) (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S R] [SMulCommClass S R R] [SMulCommClass R S R] : LinearMap.BilinForm R M →ₗ[S] QuadraticForm R M

LinearMap.BilinForm.toQuadraticForm as a linear map

Equations

• LinearMap.BilinForm.toQuadraticFormLinearMap S R M = { toFun := LinearMap.BilinForm.toQuadraticForm, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_list_sum {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : List (LinearMap.BilinForm R M)) : B.sum.toQuadraticForm = (List.map LinearMap.BilinForm.toQuadraticForm B).sum

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_multiset_sum {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : Multiset (LinearMap.BilinForm R M)) : B.sum.toQuadraticForm = (Multiset.map LinearMap.BilinForm.toQuadraticForm B).sum

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_sum {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} (s : Finset ι) (B : ι → LinearMap.BilinForm R M) : (s.sum fun (i : ι) => B i).toQuadraticForm = s.sum fun (i : ι) => (B i).toQuadraticForm

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_eq_zero {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} : B.toQuadraticForm = 0 ↔ LinearMap.IsAlt B

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_neg {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : (-B).toQuadraticForm = -B.toQuadraticForm

@[simp]

theorem LinearMap.BilinForm.toQuadraticForm_sub {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (B₁ : LinearMap.BilinForm R M) (B₂ : LinearMap.BilinForm R M) : (B₁ - B₂).toQuadraticForm = B₁.toQuadraticForm - B₂.toQuadraticForm

theorem LinearMap.BilinForm.polar_toQuadraticForm {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (x : M) (y : M) : QuadraticForm.polar (⇑B.toQuadraticForm) x y = (B x) y + (B y) x

theorem LinearMap.BilinForm.polarBilin_toQuadraticForm {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} : B.toQuadraticForm.polarBilin = B + LinearMap.flip B

@[simp]

theorem QuadraticForm.toQuadraticForm_polarBilin {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Q.polarBilin.toQuadraticForm = 2 • Q

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

theorem QuadraticForm.polarBilin_comp {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 : QuadraticForm R N) (f : M →ₗ[R] N) : (Q.comp f).polarBilin = LinearMap.compl₁₂ Q.polarBilin f f

theorem LinearMap.BilinForm.compQuadraticForm_polar {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] (f : R →ₗ[S] S) (Q : QuadraticForm R M) (x : M) (y : M) : QuadraticForm.polar (⇑(f.compQuadraticForm Q)) x y = f (QuadraticForm.polar (⇑Q) x y)

theorem LinearMap.BilinForm.compQuadraticForm_polarBilin {S : Type u_1} {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] (f : R →ₗ[S] S) (Q : QuadraticForm R M) : (f.compQuadraticForm Q).polarBilin = (LinearMap.restrictScalars₁₂ S S Q.polarBilin).compr₂ f

def QuadraticForm.associatedHom (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] : QuadraticForm R M →ₗ[S] LinearMap.BilinForm R M

associatedHom is the map that sends a quadratic form on a module M over R to its associated symmetric bilinear form. 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 QuadraticForm.associated, which gives an R-linear map. Over a general ring with no nontrivial distinguished commutative subring, use QuadraticForm.associated', which gives an additive homomorphism (or more precisely a ℤ-linear map.)

Equations

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

@[simp]

theorem QuadraticForm.associated_apply (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 : QuadraticForm R M) (x : M) (y : M) : (((QuadraticForm.associatedHom S) Q) x) y = ⅟2 * (Q (x + y) - Q x - Q y)

@[simp]

theorem QuadraticForm.two_nsmul_associated (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 : QuadraticForm R M) : 2 • (QuadraticForm.associatedHom S) Q = Q.polarBilin

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

@[simp]

theorem QuadraticForm.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] [CommSemiring S] [Algebra S R] [Invertible 2] (Q : QuadraticForm R M) [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) : (QuadraticForm.associatedHom S) (Q.comp f) = LinearMap.compl₁₂ ((QuadraticForm.associatedHom S) Q) f f

theorem QuadraticForm.associated_toQuadraticForm (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.BilinForm R M) (x : M) (y : M) : (((QuadraticForm.associatedHom S) B.toQuadraticForm) x) y = ⅟2 * ((B x) y + (B y) x)

theorem QuadraticForm.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.BilinForm R M} (h : LinearMap.IsSymm B₁) : (QuadraticForm.associatedHom S) B₁.toQuadraticForm = B₁

theorem QuadraticForm.associated_eq_self_apply (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 : QuadraticForm R M) (x : M) : (((QuadraticForm.associatedHom S) Q) x) x = Q x

theorem QuadraticForm.toQuadraticForm_associated (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 : QuadraticForm R M) : ((QuadraticForm.associatedHom S) Q).toQuadraticForm = Q

theorem QuadraticForm.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 (⇑(QuadraticForm.associatedHom S)) LinearMap.BilinForm.toQuadraticForm

@[reducible, inline]

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

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

Equations

• QuadraticForm.associated' = QuadraticForm.associatedHom ℤ

instance QuadraticForm.canLift {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] : CanLift (LinearMap.BilinForm R M) (QuadraticForm R M) (⇑(QuadraticForm.associatedHom ℕ)) LinearMap.IsSymm

Symmetric bilinear forms can be lifted to quadratic forms

Equations

• ⋯ = ⋯

theorem QuadraticForm.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₁ : QuadraticForm.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 QuadraticForm.associated {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] : QuadraticForm R M →ₗ[R] LinearMap.BilinForm R M

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

Equations

• QuadraticForm.associated = QuadraticForm.associatedHom R

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

@[simp]

theorem QuadraticForm.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) : QuadraticForm.associated (QuadraticForm.linMulLin f g) = ⅟2 • ((LinearMap.mul R R).compl₁₂ f g + (LinearMap.mul R R).compl₁₂ g f)

@[simp]

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

Orthogonality

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

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

Equations

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

theorem QuadraticForm.isOrtho_def {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} {x : M} {y : M} : Q.IsOrtho x y ↔ Q (x + y) = Q x + Q y

theorem QuadraticForm.IsOrtho.all {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) (y : M) : QuadraticForm.IsOrtho 0 x y

theorem QuadraticForm.IsOrtho.zero_left {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} (x : M) : Q.IsOrtho 0 x

theorem QuadraticForm.IsOrtho.zero_right {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} (x : M) : Q.IsOrtho x 0

theorem QuadraticForm.ne_zero_of_not_isOrtho_self {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} (x : M) (hx₁ : ¬Q.IsOrtho x x) : x ≠ 0

theorem QuadraticForm.isOrtho_comm {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} {x : M} {y : M} : Q.IsOrtho x y ↔ Q.IsOrtho y x

theorem QuadraticForm.IsOrtho.symm {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} {x : M} {y : M} : Q.IsOrtho x y → Q.IsOrtho y x

Alias of the forward direction of QuadraticForm.isOrtho_comm.

theorem LinearMap.BilinForm.toQuadraticForm_isOrtho {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [IsCancelAdd R] [NoZeroDivisors R] [CharZero R] {B : LinearMap.BilinForm R M} {x : M} {y : M} (h : LinearMap.IsSymm B) : B.toQuadraticForm.IsOrtho x y ↔ LinearMap.IsOrtho B x y

@[simp]

theorem QuadraticForm.isOrtho_polarBilin {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : M} {y : M} : LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y

theorem QuadraticForm.IsOrtho.polar_eq_zero {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : M} {y : M} (h : Q.IsOrtho x y) : QuadraticForm.polar (⇑Q) x y = 0

@[simp]

theorem QuadraticForm.associated_isOrtho {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {x : M} {y : M} : LinearMap.IsOrtho (QuadraticForm.associated Q) x y ↔ Q.IsOrtho x y

def QuadraticForm.Anisotropic {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : Prop

An anisotropic quadratic form is zero only on zero vectors.

Equations

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

theorem QuadraticForm.not_anisotropic_iff_exists {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : ¬Q.Anisotropic ↔ ∃ (x : M), x ≠ 0 ∧ Q x = 0

theorem QuadraticForm.Anisotropic.eq_zero_iff {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} (h : Q.Anisotropic) {x : M} : Q x = 0 ↔ x = 0

theorem QuadraticForm.separatingLeft_of_anisotropic {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (hB : Q.Anisotropic) : LinearMap.SeparatingLeft (QuadraticForm.associated' Q)

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

def QuadraticForm.PosDef {M : Type u_4} {R₂ : Type u} [OrderedCommRing R₂] [AddCommMonoid M] [Module R₂ M] (Q₂ : QuadraticForm R₂ M) : Prop

A positive definite quadratic form is positive on nonzero vectors.

Equations

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

theorem QuadraticForm.PosDef.smul {M : Type u_4} [AddCommMonoid M] {R : Type u_6} [LinearOrderedCommRing R] [Module R M] {Q : QuadraticForm R M} (h : Q.PosDef) {a : R} (a_pos : 0 < a) : (a • Q).PosDef

theorem QuadraticForm.PosDef.nonneg {M : Type u_4} {R₂ : Type u} [OrderedCommRing R₂] [AddCommMonoid M] [Module R₂ M] {Q : QuadraticForm R₂ M} (hQ : Q.PosDef) (x : M) : 0 ≤ Q x

theorem QuadraticForm.PosDef.anisotropic {M : Type u_4} {R₂ : Type u} [OrderedCommRing R₂] [AddCommMonoid M] [Module R₂ M] {Q : QuadraticForm R₂ M} (hQ : Q.PosDef) : Q.Anisotropic

theorem QuadraticForm.posDef_of_nonneg {M : Type u_4} {R₂ : Type u} [OrderedCommRing R₂] [AddCommMonoid M] [Module R₂ M] {Q : QuadraticForm R₂ M} (h : ∀ (x : M), 0 ≤ Q x) (h0 : Q.Anisotropic) : Q.PosDef

theorem QuadraticForm.posDef_iff_nonneg {M : Type u_4} {R₂ : Type u} [OrderedCommRing R₂] [AddCommMonoid M] [Module R₂ M] {Q : QuadraticForm R₂ M} : Q.PosDef ↔ (∀ (x : M), 0 ≤ Q x) ∧ Q.Anisotropic

theorem QuadraticForm.PosDef.add {M : Type u_4} {R₂ : Type u} [OrderedCommRing R₂] [AddCommMonoid M] [Module R₂ M] (Q : QuadraticForm R₂ M) (Q' : QuadraticForm R₂ M) (hQ : Q.PosDef) (hQ' : Q'.PosDef) : (Q + Q').PosDef

theorem QuadraticForm.linMulLinSelfPosDef {M : Type u_4} [AddCommMonoid M] {R : Type u_7} [LinearOrderedCommRing R] [Module R M] (f : M →ₗ[R] R) (hf : LinearMap.ker f = ⊥) : (QuadraticForm.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.toQuadraticForm' {R : Type u_3} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : QuadraticForm R (n → R)

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

Equations

• M.toQuadraticForm' = LinearMap.BilinForm.toQuadraticForm (Matrix.toLinearMap₂' M)

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

A matrix representation of the quadratic form.

Equations

• Q.toMatrix' = LinearMap.toMatrix₂' (QuadraticForm.associated Q)

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

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

@[simp]

theorem QuadraticForm.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 : QuadraticForm R (m → R)) (f : (n → R) →ₗ[R] m → R) : (Q.comp f).toMatrix' = (LinearMap.toMatrix' f).transpose * Q.toMatrix' * LinearMap.toMatrix' f

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

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

Equations

• Q.discr = Q.toMatrix'.det

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

theorem QuadraticForm.discr_comp {R : Type u_3} {n : Type w} [Fintype n] [CommRing R] [DecidableEq n] [Invertible 2] {Q : QuadraticForm R (n → 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 : B.toQuadraticForm.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 QuadraticForm.basisRepr {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} [Finite ι] (Q : QuadraticForm R M) (v : Basis ι R M) : QuadraticForm R (ι → R)

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

Equations

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

@[simp]

theorem QuadraticForm.basisRepr_apply {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} [Fintype ι] {v : Basis ι R M} (Q : QuadraticForm R M) (w : ι → R) : (Q.basisRepr v) w = Q (Finset.univ.sum fun (i : ι) => w i • v i)

def QuadraticForm.weightedSumSquares {S : Type u_1} (R : Type u_3) [CommSemiring R] {ι : Type u_6} [Fintype ι] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) : QuadraticForm 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

• QuadraticForm.weightedSumSquares R w = Finset.univ.sum fun (i : ι) => w i • QuadraticForm.proj i i

@[simp]

theorem QuadraticForm.weightedSumSquares_apply {S : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_6} [Fintype ι] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) (v : ι → R) : (QuadraticForm.weightedSumSquares R w) v = Finset.univ.sum fun (i : ι) => w i • (v i * v i)

theorem QuadraticForm.basisRepr_eq_of_iIsOrtho {ι : Type u_6} [Fintype ι] {R : Type u_7} {M : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (v : Basis ι R M) (hv₂ : LinearMap.IsOrthoᵢ (QuadraticForm.associated Q) ⇑v) : Q.basisRepr v = QuadraticForm.weightedSumSquares R fun (i : ι) => Q (v i)

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