Documentation

Mathlib.LinearAlgebra.QuadraticForm.Basic

Quadratic forms #

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

This notion generalizes to 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 #

Main statements #

Notation #

In this file, the variable R is used when a Ring structure is sufficient and R₁ is used when specifically a CommRing is required. This allows us to keep [Module R M] and [Module R₁ M] assumptions in the variables without confusion between * from Ring and * from CommRing.

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

References #

Tags #

quadratic form, homogeneous polynomial, quadratic polynomial

def QuadraticForm.polar {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] (f : MR) (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

Instances For
    theorem QuadraticForm.polar_add {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] (f : MR) (g : MR) (x : M) (y : M) :
    theorem QuadraticForm.polar_neg {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] (f : MR) (x : M) (y : M) :
    theorem QuadraticForm.polar_smul {S : Type u_1} {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Monoid S] [DistribMulAction S R] (f : MR) (s : S) (x : M) (y : M) :
    theorem QuadraticForm.polar_comm {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] (f : MR) (x : M) (y : M) :
    theorem QuadraticForm.polar_add_left_iff {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] {f : MR} {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_5} [Ring R] [AddCommGroup M] {F : Type u_6} [Ring S] [AddMonoidHomClass F R S] (f : MR) (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) [Semiring 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.

    Instances For
      instance QuadraticForm.funLike {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
      FunLike (QuadraticForm R M) M fun x => R
      instance QuadraticForm.instCoeFunQuadraticFormForAll {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
      CoeFun (QuadraticForm R M) fun x => MR

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

      @[simp]
      theorem QuadraticForm.toFun_eq_coe {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) :
      Q.toFun = Q

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

      theorem QuadraticForm.ext {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Semiring 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_5} [Semiring 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_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (Q' : MR) (h : Q' = Q) :

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

      Instances For
        @[simp]
        theorem QuadraticForm.coe_copy {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (Q' : MR) (h : Q' = Q) :
        ↑(QuadraticForm.copy Q Q' h) = Q'
        theorem QuadraticForm.copy_eq {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (Q' : MR) (h : Q' = Q) :
        theorem QuadraticForm.map_smul {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) :
        B, ∀ (x y : M), Q (x + y) = Q x + Q y + BilinForm.bilin B x y
        theorem QuadraticForm.map_add_add_add_map {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Semiring 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_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) :
        Q 0 = 0
        theorem QuadraticForm.map_smul_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Ring 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_5} [Ring 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_5} [Ring 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_5} [Ring 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_5} [Ring 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_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) (y : M) :
        @[simp]
        theorem QuadraticForm.polar_sub_left {R : Type u_3} {M : Type u_5} [Ring 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_5} [Ring 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_5} [Ring 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_5} [Ring 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_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) (y : M) :
        @[simp]
        theorem QuadraticForm.polar_sub_right {R : Type u_3} {M : Type u_5} [Ring 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_5} [Ring 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 {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) (y : M) :
        def QuadraticForm.polarBilin {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :

        QuadraticForm.polar as a bilinear form

        Instances For
          @[simp]
          theorem QuadraticForm.polar_smul_left_of_tower {S : Type u_1} {R : Type u_3} {M : Type u_5} [Ring 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_5} [Ring 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_5} [Ring R] [AddCommGroup M] [Module R M] (toFun : MR) (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_5} [Ring R] [AddCommGroup M] [Module R M] (toFun : MR) (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) :

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

          Instances For
            theorem QuadraticForm.choose_exists_companion {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
            Exists.choose (_ : B, ∀ (x y : M), Q (x + y) = Q x + Q y + BilinForm.bilin B x y) = QuadraticForm.polarBilin Q

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

            instance QuadraticForm.instSMulQuadraticForm {S : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] :

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

            When R is commutative, this provides an R-action via Algebra.id.

            @[simp]
            theorem QuadraticForm.coeFn_smul {S : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Semiring 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
            @[simp]
            theorem QuadraticForm.coeFn_zero {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
            0 = 0
            @[simp]
            theorem QuadraticForm.zero_apply {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
            0 x = 0
            @[simp]
            theorem QuadraticForm.coeFn_add {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (x : M) :
            ↑(Q + Q') x = Q x + Q' x
            @[simp]
            theorem QuadraticForm.coeFnAddMonoidHom_apply {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Semiring R] [AddCommMonoid M] [Module R M] :
            QuadraticForm R M →+ MR

            @CoeFn (QuadraticForm R M) as an AddMonoidHom.

            This API mirrors AddMonoidHom.coeFn.

            Instances For
              @[simp]
              theorem QuadraticForm.evalAddMonoidHom_apply {R : Type u_3} {M : Type u_5} [Semiring 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_5} [Semiring R] [AddCommMonoid M] [Module R M] (m : M) :

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

              Instances For
                @[simp]
                theorem QuadraticForm.coeFn_sum {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} (Q : ιQuadraticForm R M) (s : Finset ι) :
                ↑(Finset.sum s fun i => Q i) = Finset.sum s fun i => ↑(Q i)
                @[simp]
                theorem QuadraticForm.sum_apply {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} (Q : ιQuadraticForm R M) (s : Finset ι) (x : M) :
                ↑(Finset.sum s fun i => Q i) x = Finset.sum s fun i => ↑(Q i) x
                @[simp]
                theorem QuadraticForm.coeFn_neg {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
                ↑(-Q) = -Q
                @[simp]
                theorem QuadraticForm.neg_apply {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M) :
                ↑(-Q) x = -Q x
                @[simp]
                theorem QuadraticForm.coeFn_sub {R : Type u_3} {M : Type u_5} [Ring 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_5} [Ring R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (x : M) :
                ↑(Q - Q') x = Q x - Q' x
                def QuadraticForm.comp {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type v} [AddCommMonoid N] [Module R N] (Q : QuadraticForm R N) (f : M →ₗ[R] N) :

                Compose the quadratic form with a linear function.

                Instances For
                  @[simp]
                  theorem QuadraticForm.comp_apply {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type v} [AddCommMonoid N] [Module R N] (Q : QuadraticForm R N) (f : M →ₗ[R] N) (x : M) :
                  ↑(QuadraticForm.comp Q f) x = Q (f x)
                  @[simp]
                  theorem LinearMap.compQuadraticForm_apply {S : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring 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) :
                  ↑(LinearMap.compQuadraticForm f Q) x = f (Q x)
                  def LinearMap.compQuadraticForm {S : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring 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) :

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

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

                    The product of linear forms is a quadratic form.

                    Instances For
                      @[simp]
                      theorem QuadraticForm.linMulLin_apply {R : Type u_3} {M : Type u_5} [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]
                      @[simp]
                      @[simp]
                      theorem QuadraticForm.sq_apply {R : Type u_3} [CommSemiring R] (a : R) :
                      QuadraticForm.sq a = a * a

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

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

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

                        Instances For
                          @[simp]
                          theorem QuadraticForm.proj_apply {R : Type u_3} [CommSemiring R] {n : Type u_6} (i : n) (j : n) (x : nR) :
                          ↑(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 BilinForm.toQuadraticForm {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) :

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

                          Instances For
                            @[simp]
                            theorem BilinForm.toQuadraticForm_apply {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (x : M) :
                            @[simp]
                            @[simp]
                            theorem BilinForm.toQuadraticForm_smul {S : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (a : S) (B : BilinForm R M) :

                            BilinForm.toQuadraticForm as an additive homomorphism

                            Instances For
                              @[simp]
                              theorem BilinForm.toQuadraticFormLinearMap_apply_apply (S : Type u_1) (R : Type u_3) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S R] [SMulCommClass S R R] (B : BilinForm R M) (x : M) :
                              def BilinForm.toQuadraticFormLinearMap (S : Type u_1) (R : Type u_3) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S R] [SMulCommClass S R R] :

                              BilinForm.toQuadraticForm as a linear map

                              Instances For
                                @[simp]
                                theorem BilinForm.toQuadraticForm_list_sum {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (B : List (BilinForm R M)) :
                                BilinForm.toQuadraticForm (List.sum B) = List.sum (List.map BilinForm.toQuadraticForm B)
                                @[simp]
                                @[simp]
                                theorem BilinForm.toQuadraticForm_sum {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_6} (s : Finset ι) (B : ιBilinForm R M) :
                                @[simp]
                                theorem BilinForm.toQuadraticForm_sub {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (B₁ : BilinForm R M) (B₂ : BilinForm R M) :
                                theorem BilinForm.polar_toQuadraticForm {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {B : BilinForm R M} (x : M) (y : M) :
                                theorem BilinForm.polarBilin_toQuadraticForm {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {B : BilinForm R M} :
                                theorem QuadraticForm.polarBilin_injective {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (h : IsUnit 2) :
                                Function.Injective QuadraticForm.polarBilin
                                theorem LinearMap.compQuadraticForm_polar {S : Type u_1} {R : Type u_3} {M : Type u_5} [Ring 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) :
                                def QuadraticForm.associatedHom (S : Type u_1) {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] :

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

                                Instances For
                                  @[simp]
                                  theorem QuadraticForm.associated_apply (S : Type u_1) {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] (Q : QuadraticForm R M) (x : M) (y : M) :
                                  BilinForm.bilin (↑(QuadraticForm.associatedHom S) Q) x y = 2 * (Q (x + y) - Q x - Q y)
                                  @[simp]
                                  theorem QuadraticForm.associated_comp (S : Type u_1) {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] (Q : QuadraticForm R M) {N : Type v} [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) :
                                  theorem QuadraticForm.associated_left_inverse (S : Type u_1) {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] {B₁ : BilinForm R M} (h : BilinForm.IsSymm B₁) :
                                  theorem QuadraticForm.associated_eq_self_apply (S : Type u_1) {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] (Q : QuadraticForm R M) (x : M) :
                                  theorem QuadraticForm.associated_rightInverse (S : Type u_1) {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] :
                                  Function.RightInverse (↑(QuadraticForm.associatedHom S)) BilinForm.toQuadraticForm
                                  @[inline, reducible]

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

                                  Instances For
                                    instance QuadraticForm.canLift {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [Invertible 2] :
                                    CanLift (BilinForm R M) (QuadraticForm R M) (↑(QuadraticForm.associatedHom )) BilinForm.IsSymm

                                    Symmetric bilinear forms can be lifted to quadratic forms

                                    theorem QuadraticForm.exists_quadraticForm_ne_zero {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (hB₁ : QuadraticForm.associated' Q 0) :
                                    x, 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.

                                    @[inline, reducible]
                                    abbrev QuadraticForm.associated {R₁ : Type u_4} {M : Type u_5} [CommRing R₁] [AddCommGroup M] [Module R₁ M] [Invertible 2] :
                                    QuadraticForm R₁ M →ₗ[R₁] BilinForm R₁ M

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

                                    Instances For
                                      theorem QuadraticForm.coe_associatedHom (S : Type u_1) {R₁ : Type u_4} {M : Type u_5} [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_4} {M : Type u_5} [CommRing R₁] [AddCommGroup M] [Module R₁ M] [Invertible 2] (f : M →ₗ[R₁] R₁) (g : M →ₗ[R₁] R₁) :
                                      QuadraticForm.associated (QuadraticForm.linMulLin f g) = 2 (BilinForm.linMulLin f g + BilinForm.linMulLin g f)
                                      @[simp]
                                      theorem QuadraticForm.associated_sq {R₁ : Type u_4} [CommRing R₁] [Invertible 2] :
                                      QuadraticForm.associated QuadraticForm.sq = LinearMap.toBilin (LinearMap.mul R₁ R₁)
                                      def QuadraticForm.Anisotropic {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) :

                                      An anisotropic quadratic form is zero only on zero vectors.

                                      Instances For
                                        theorem QuadraticForm.Anisotropic.eq_zero_iff {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticForm R M} (h : QuadraticForm.Anisotropic Q) {x : M} :
                                        Q x = 0 x = 0
                                        theorem QuadraticForm.nondegenerate_of_anisotropic {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (hB : QuadraticForm.Anisotropic Q) :
                                        BilinForm.Nondegenerate (QuadraticForm.associated' Q)

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

                                        def QuadraticForm.PosDef {M : Type u_5} {R₂ : Type u} [OrderedRing R₂] [AddCommMonoid M] [Module R₂ M] (Q₂ : QuadraticForm R₂ M) :

                                        A positive definite quadratic form is positive on nonzero vectors.

                                        Instances For
                                          theorem QuadraticForm.PosDef.smul {M : Type u_5} [AddCommMonoid M] {R : Type u_6} [LinearOrderedCommRing R] [Module R M] {Q : QuadraticForm R M} (h : QuadraticForm.PosDef Q) {a : R} (a_pos : 0 < a) :
                                          theorem QuadraticForm.PosDef.nonneg {M : Type u_5} {R₂ : Type u} [OrderedRing R₂] [AddCommMonoid M] [Module R₂ M] {Q : QuadraticForm R₂ M} (hQ : QuadraticForm.PosDef Q) (x : M) :
                                          0 Q x
                                          theorem QuadraticForm.posDef_of_nonneg {M : Type u_5} {R₂ : Type u} [OrderedRing R₂] [AddCommMonoid M] [Module R₂ M] {Q : QuadraticForm R₂ M} (h : ∀ (x : M), 0 Q x) (h0 : QuadraticForm.Anisotropic Q) :
                                          theorem QuadraticForm.posDef_iff_nonneg {M : Type u_5} {R₂ : Type u} [OrderedRing R₂] [AddCommMonoid M] [Module R₂ M] {Q : QuadraticForm R₂ M} :
                                          theorem QuadraticForm.PosDef.add {M : Type u_5} {R₂ : Type u} [OrderedRing R₂] [AddCommMonoid M] [Module R₂ M] (Q : QuadraticForm R₂ M) (Q' : QuadraticForm R₂ M) (hQ : QuadraticForm.PosDef Q) (hQ' : QuadraticForm.PosDef Q') :

                                          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_4} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R₁] (M : Matrix n n R₁) :
                                          QuadraticForm R₁ (nR₁)

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

                                          Instances For
                                            def QuadraticForm.toMatrix' {R₁ : Type u_4} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R₁] [Invertible 2] (Q : QuadraticForm R₁ (nR₁)) :
                                            Matrix n n R₁

                                            A matrix representation of the quadratic form.

                                            Instances For
                                              theorem QuadraticForm.toMatrix'_smul {R₁ : Type u_4} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R₁] [Invertible 2] (a : R₁) (Q : QuadraticForm R₁ (nR₁)) :
                                              theorem QuadraticForm.isSymm_toMatrix' {R₁ : Type u_4} {n : Type w} [Fintype n] [DecidableEq n] [CommRing R₁] [Invertible 2] (Q : QuadraticForm R₁ (nR₁)) :
                                              @[simp]
                                              theorem QuadraticForm.toMatrix'_comp {R₁ : Type u_4} {n : Type w} [Fintype n] [CommRing R₁] [DecidableEq n] [Invertible 2] {m : Type w} [DecidableEq m] [Fintype m] (Q : QuadraticForm R₁ (mR₁)) (f : (nR₁) →ₗ[R₁] mR₁) :
                                              QuadraticForm.toMatrix' (QuadraticForm.comp Q f) = Matrix.transpose (LinearMap.toMatrix' f) * QuadraticForm.toMatrix' Q * LinearMap.toMatrix' f
                                              def QuadraticForm.discr {R₁ : Type u_4} {n : Type w} [Fintype n] [CommRing R₁] [DecidableEq n] [Invertible 2] (Q : QuadraticForm R₁ (nR₁)) :
                                              R₁

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

                                              Instances For
                                                theorem QuadraticForm.discr_smul {R₁ : Type u_4} {n : Type w} [Fintype n] [CommRing R₁] [DecidableEq n] [Invertible 2] {Q : QuadraticForm R₁ (nR₁)} (a : R₁) :
                                                theorem QuadraticForm.discr_comp {R₁ : Type u_4} {n : Type w} [Fintype n] [CommRing R₁] [DecidableEq n] [Invertible 2] {Q : QuadraticForm R₁ (nR₁)} (f : (nR₁) →ₗ[R₁] nR₁) :
                                                QuadraticForm.discr (QuadraticForm.comp Q f) = Matrix.det (LinearMap.toMatrix' f) * Matrix.det (LinearMap.toMatrix' f) * QuadraticForm.discr Q

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

                                                theorem BilinForm.exists_bilinForm_self_ne_zero {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [htwo : Invertible 2] {B : BilinForm R M} (hB₁ : B 0) (hB₂ : BilinForm.IsSymm B) :
                                                x, ¬BilinForm.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 BilinForm.exists_orthogonal_basis {V : Type u} {K : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [hK : Invertible 2] {B : BilinForm K V} (hB₂ : BilinForm.IsSymm B) :
                                                v, BilinForm.iIsOrtho 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_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_7} [Fintype ι] (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.

                                                Instances For
                                                  @[simp]
                                                  theorem QuadraticForm.basisRepr_apply {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_7} [Fintype ι] {v : Basis ι R M} (Q : QuadraticForm R M) (w : ιR) :
                                                  ↑(QuadraticForm.basisRepr Q v) w = Q (Finset.sum Finset.univ fun i => w i v i)
                                                  def QuadraticForm.weightedSumSquares {S : Type u_1} (R₁ : Type u_4) [CommSemiring R₁] {ι : Type u_7} [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.

                                                  Instances For
                                                    @[simp]
                                                    theorem QuadraticForm.weightedSumSquares_apply {S : Type u_1} {R₁ : Type u_4} [CommSemiring R₁] {ι : Type u_7} [Fintype ι] [Monoid S] [DistribMulAction S R₁] [SMulCommClass S R₁ R₁] (w : ιS) (v : ιR₁) :
                                                    ↑(QuadraticForm.weightedSumSquares R₁ w) v = Finset.sum Finset.univ fun i => w i (v i * v i)
                                                    theorem QuadraticForm.basisRepr_eq_of_iIsOrtho {ι : Type u_7} [Fintype ι] {R₁ : Type u_8} {M : Type u_9} [CommRing R₁] [AddCommGroup M] [Module R₁ M] [Invertible 2] (Q : QuadraticForm R₁ M) (v : Basis ι R₁ M) (hv₂ : BilinForm.iIsOrtho (QuadraticForm.associated Q) v) :

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