Documentation

Mathlib.LinearAlgebra.QuadraticForm.Basic

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:

This notion generalizes to commutative semirings using the approach in [izhakian2016][] 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 #

Main statements #

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 #

Tags #

quadratic map, homogeneous polynomial, quadratic polynomial

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

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

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

Equations
Instances For
    theorem QuadraticMap.map_add {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : MN) (x : M) (y : M) :
    f (x + y) = f x + f y + QuadraticMap.polar f x y
    theorem QuadraticMap.polar_add {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : MN) (g : MN) (x : M) (y : M) :
    theorem QuadraticMap.polar_neg {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : MN) (x : M) (y : M) :
    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 : MN) (s : S) (x : M) (y : M) :
    theorem QuadraticMap.polar_comm {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] (f : MN) (x : M) (y : M) :
    theorem QuadraticMap.polar_add_left_iff {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] {f : MN} {x : M} {x' : M} {y : M} :
    QuadraticMap.polar f (x + x') y = QuadraticMap.polar f x y + QuadraticMap.polar f x' y f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

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

    theorem QuadraticMap.polar_comp {S : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] {F : Type u_8} [CommRing S] [FunLike F N S] [AddMonoidHomClass F N S] (f : MN) (g : F) (x : M) (y : M) :
    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 : MN
    • 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
    Instances For
      theorem QuadraticMap.toFun_smul {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (self : QuadraticMap R M N) (a : R) (x : M) :
      self.toFun (a x) = (a * a) self.toFun x
      theorem QuadraticMap.exists_companion' {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (self : QuadraticMap R M N) :
      ∃ (B : LinearMap.BilinMap R M N), ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B x) y
      @[reducible, inline]
      abbrev QuadraticForm (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :
      Type (max u v)

      A quadratic form on a module.

      Equations
      Instances For
        instance QuadraticMap.instFunLike {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
        FunLike (QuadraticMap R M N) M N
        Equations
        • QuadraticMap.instFunLike = { coe := QuadraticMap.toFun, coe_injective' := }
        instance QuadraticMap.instCoeFunForall {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
        CoeFun (QuadraticMap R M N) fun (x : QuadraticMap R M N) => MN

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

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

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

        theorem QuadraticMap.ext_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} :
        Q = Q' ∀ (x : M), Q x = Q' x
        theorem QuadraticMap.ext {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} (H : ∀ (x : M), Q x = Q' x) :
        Q = Q'
        theorem QuadraticMap.congr_fun {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {Q' : QuadraticMap R M N} (h : Q = Q') (x : M) :
        Q x = Q' x
        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' : MN) (h : Q' = Q) :

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

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

          QuadraticMap.polar as a bilinear map

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

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

            Equations
            • QuadraticMap.ofPolar toFun toFun_smul polar_add_left polar_smul_left = { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := }
            Instances For
              theorem QuadraticMap.choose_exists_companion {R : Type u_3} {M : Type u_4} {N : Type u_5} [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 (∑ is, f i) = is, Q (f i) + ijFinset.filter (fun (x : Sym2 ι) => ¬x.IsDiag) s.sym2, Sym2.lift fun (i j : ι) => QuadraticMap.polar (⇑Q) (f i) (f j), ij
              theorem QuadraticMap.map_sum' {R : Type u_3} {M : Type u_4} {N : Type u_5} [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 (∑ is, f i) = ijs.sym2, Sym2.lift fun (i j : ι) => QuadraticMap.polar (⇑Q) (f i) (f j), ij - is, Q (f i)
              instance QuadraticMap.instSMul {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [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] :
              Equations
              • =
              instance QuadraticMap.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [Monoid T] [DistribMulAction S N] [DistribMulAction T N] [SMulCommClass S R N] [SMulCommClass T R N] [SMul S T] [IsScalarTower S T N] :
              Equations
              • =
              instance QuadraticMap.instZero {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
              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] :
              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] :
              Equations
              • QuadraticMap.instAdd = { add := fun (Q Q' : QuadraticMap R M N) => { toFun := Q + Q', toFun_smul := , exists_companion' := } }
              @[simp]
              theorem QuadraticMap.coeFn_add {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) :
              (Q + Q') = Q + Q'
              @[simp]
              theorem QuadraticMap.add_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) (x : M) :
              (Q + Q') x = Q x + Q' x
              instance QuadraticMap.instAddCommMonoid {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
              Equations
              @[simp]
              theorem QuadraticMap.coeFnAddMonoidHom_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
              ∀ (a : QuadraticMap R M N) (a_1 : M), QuadraticMap.coeFnAddMonoidHom a a_1 = a a_1
              def QuadraticMap.coeFnAddMonoidHom {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
              QuadraticMap R M N →+ MN

              @CoeFn (QuadraticMap R M) as an AddMonoidHom.

              This API mirrors AddMonoidHom.coeFn.

              Equations
              • QuadraticMap.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
              Instances For
                @[simp]
                theorem QuadraticMap.evalAddMonoidHom_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) :
                ∀ (a : QuadraticMap R M N), (QuadraticMap.evalAddMonoidHom m) a = a m
                def QuadraticMap.evalAddMonoidHom {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) :

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

                Equations
                Instances For
                  @[simp]
                  theorem QuadraticMap.coeFn_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_8} (Q : ιQuadraticMap R M N) (s : Finset ι) :
                  (∑ is, Q i) = is, (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) :
                  (∑ is, Q i) x = is, (Q i) x
                  Equations
                  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] :
                  Equations
                  • QuadraticMap.instModuleOfSMulCommClass = Module.mk
                  instance QuadraticMap.instNeg {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :
                  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] :
                  Equations
                  • QuadraticMap.instSub = { sub := fun (Q Q' : QuadraticMap R M N) => (Q + -Q').copy (Q - Q') }
                  @[simp]
                  theorem QuadraticMap.coeFn_sub {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) :
                  (Q - Q') = Q - Q'
                  @[simp]
                  theorem QuadraticMap.sub_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M N) (x : M) :
                  (Q - Q') x = Q x - Q' x
                  instance QuadraticMap.instAddCommGroup {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :
                  Equations
                  @[simp]
                  theorem QuadraticMap.restrictScalars_apply {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S M] [Module S N] [Algebra S R] [IsScalarTower S R M] [IsScalarTower S R N] (Q : QuadraticMap R M N) (x : M) :
                  Q.restrictScalars x = Q x
                  def QuadraticMap.restrictScalars {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S M] [Module S N] [Algebra S R] [IsScalarTower S R M] [IsScalarTower S R N] (Q : QuadraticMap R M N) :

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

                  Equations
                  • Q.restrictScalars = { toFun := fun (x : M) => Q x, toFun_smul := , exists_companion' := }
                  Instances For
                    def QuadraticMap.comp {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [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) :

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

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

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

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

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

                        Equations
                        • f.compQuadraticMap' Q = f.compQuadraticMap Q.restrictScalars
                        Instances For
                          def QuadraticMap.linMulLin {R : Type u_3} {M : Type u_4} {A : Type u_7} [CommSemiring R] [NonUnitalNonAssocSemiring A] [AddCommMonoid M] [Module R M] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A) (g : M →ₗ[R] A) :

                          The product of linear forms is a quadratic form.

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

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

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

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

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

                                Associated bilinear maps #

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

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

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

                                Equations
                                • B.toQuadraticMap = { toFun := fun (x : M) => (B x) x, toFun_smul := , exists_companion' := }
                                Instances For
                                  @[simp]
                                  theorem LinearMap.BilinMap.toQuadraticMap_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [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) :
                                  @[simp]
                                  theorem LinearMap.BilinMap.toQuadraticMap_add {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B₁ : LinearMap.BilinMap R M N) (B₂ : LinearMap.BilinMap R M N) :
                                  (B₁ + B₂).toQuadraticMap = B₁.toQuadraticMap + B₂.toQuadraticMap
                                  @[simp]
                                  theorem LinearMap.BilinMap.toQuadraticMap_smul {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] [SMulCommClass R S N] (a : S) (B : LinearMap.BilinMap R M N) :
                                  (a B).toQuadraticMap = a B.toQuadraticMap

                                  LinearMap.BilinForm.toQuadraticMap as an additive homomorphism

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem LinearMap.BilinMap.toQuadraticMapLinearMap_apply_apply (S : Type u_1) (R : Type u_3) (M : Type u_4) {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass S R N] [SMulCommClass R S N] (B : LinearMap.BilinMap R M N) (x : M) :
                                    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.BilinForm.toQuadraticMap as a linear map

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem LinearMap.BilinMap.toQuadraticMap_list_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : List (LinearMap.BilinMap R M N)) :
                                      B.sum.toQuadraticMap = (List.map LinearMap.BilinMap.toQuadraticMap B).sum
                                      @[simp]
                                      theorem LinearMap.BilinMap.toQuadraticMap_multiset_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : Multiset (LinearMap.BilinMap R M N)) :
                                      B.sum.toQuadraticMap = (Multiset.map LinearMap.BilinMap.toQuadraticMap B).sum
                                      @[simp]
                                      theorem LinearMap.BilinMap.toQuadraticMap_sum {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_9} (s : Finset ι) (B : ιLinearMap.BilinMap R M N) :
                                      (∑ is, B i).toQuadraticMap = is, (B i).toQuadraticMap
                                      @[simp]
                                      theorem LinearMap.BilinMap.toQuadraticMap_eq_zero {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {B : LinearMap.BilinMap R M N} :
                                      B.toQuadraticMap = 0 LinearMap.IsAlt B
                                      @[simp]
                                      theorem LinearMap.BilinMap.toQuadraticMap_neg {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (B : LinearMap.BilinMap R M N) :
                                      (-B).toQuadraticMap = -B.toQuadraticMap
                                      @[simp]
                                      theorem LinearMap.BilinMap.toQuadraticMap_sub {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (B₁ : LinearMap.BilinMap R M N) (B₂ : LinearMap.BilinMap R M N) :
                                      (B₁ - B₂).toQuadraticMap = B₁.toQuadraticMap - B₂.toQuadraticMap
                                      theorem LinearMap.BilinMap.polar_toQuadraticMap {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {B : LinearMap.BilinMap R M N} (x : M) (y : M) :
                                      QuadraticMap.polar (⇑B.toQuadraticMap) x y = (B x) y + (B y) x
                                      theorem LinearMap.BilinMap.polarBilin_toQuadraticMap {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {B : LinearMap.BilinMap R M N} :
                                      B.toQuadraticMap.polarBilin = B + LinearMap.flip B
                                      @[simp]
                                      theorem QuadraticMap.toQuadraticMap_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) :
                                      Q.polarBilin.toQuadraticMap = 2 Q
                                      theorem QuadraticMap.polarBilin_injective {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (h : IsUnit 2) :
                                      Function.Injective QuadraticMap.polarBilin
                                      theorem QuadraticMap.polarBilin_comp {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {N' : Type u_8} [AddCommGroup N'] [Module R N'] (Q : QuadraticMap R N' N) (f : M →ₗ[R] N') :
                                      (Q.comp f).polarBilin = LinearMap.compl₁₂ Q.polarBilin f f
                                      theorem LinearMap.compQuadraticMap_polar {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {N' : Type u_8} [AddCommGroup N'] [CommSemiring S] [Algebra S R] [Module S N] [Module S N'] [IsScalarTower S R N] [Module S M] [IsScalarTower S R M] (f : N →ₗ[S] N') (Q : QuadraticMap R M N) (x : M) (y : M) :
                                      QuadraticMap.polar (⇑(f.compQuadraticMap' Q)) x y = f (QuadraticMap.polar (⇑Q) x y)
                                      theorem LinearMap.compQuadraticMap_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {N' : Type u_8} [AddCommGroup N'] [Module R N'] (f : N →ₗ[R] N') (Q : QuadraticMap R M N) :
                                      (f.compQuadraticMap' Q).polarBilin = LinearMap.compr₂ Q.polarBilin f
                                      def QuadraticMap.associatedHom (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] :

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

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

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem QuadraticMap.associated_apply (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) (x : M) (y : M) :
                                        (((QuadraticMap.associatedHom S) Q) x) y = 2 (Q (x + y) - Q x - Q y)
                                        @[simp]
                                        theorem QuadraticMap.two_nsmul_associated (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) :
                                        2 (QuadraticMap.associatedHom S) Q = Q.polarBilin
                                        @[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) :
                                        theorem QuadraticMap.associated_toQuadraticMap (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] (B : LinearMap.BilinMap R M R) (x : M) (y : M) :
                                        (((QuadraticMap.associatedHom S) B.toQuadraticMap) x) y = 2 ((B x) y + (B y) x)
                                        theorem QuadraticMap.associated_left_inverse (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] {B₁ : LinearMap.BilinMap R M R} (h : LinearMap.IsSymm B₁) :
                                        (QuadraticMap.associatedHom S) B₁.toQuadraticMap = B₁
                                        theorem QuadraticMap.associated_eq_self_apply (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) (x : M) :
                                        (((QuadraticMap.associatedHom S) Q) x) x = Q x
                                        theorem QuadraticMap.toQuadraticMap_associated (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CommSemiring S] [Algebra S R] [Module S N] [IsScalarTower S R N] [Invertible 2] (Q : QuadraticMap R M N) :
                                        ((QuadraticMap.associatedHom S) Q).toQuadraticMap = Q
                                        theorem QuadraticMap.associated_rightInverse (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] :
                                        Function.RightInverse (⇑(QuadraticMap.associatedHom S)) LinearMap.BilinMap.toQuadraticMap
                                        @[reducible, inline]

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

                                        Equations
                                        Instances For
                                          instance QuadraticMap.canLift {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] :

                                          Symmetric bilinear forms can be lifted to quadratic forms

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

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

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

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

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

                                            Orthogonality #

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

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

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

                                              Alias of the forward direction of QuadraticMap.isOrtho_comm.

                                              theorem LinearMap.BilinForm.toQuadraticMap_isOrtho {R : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [IsCancelAdd R] [NoZeroDivisors R] [CharZero R] {B : LinearMap.BilinMap R M R} {x : M} {y : M} (h : LinearMap.IsSymm B) :
                                              B.toQuadraticMap.IsOrtho x y LinearMap.IsOrtho B x y
                                              @[simp]
                                              theorem QuadraticMap.isOrtho_polarBilin {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} :
                                              LinearMap.IsOrtho Q.polarBilin x y Q.IsOrtho x y
                                              theorem QuadraticMap.IsOrtho.polar_eq_zero {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} {x : M} {y : M} (h : Q.IsOrtho x y) :
                                              QuadraticMap.polar (⇑Q) x y = 0
                                              @[simp]
                                              theorem QuadraticMap.associated_isOrtho {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} [Invertible 2] {x : M} {y : M} :
                                              LinearMap.IsOrtho (QuadraticMap.associated Q) x y Q.IsOrtho x y
                                              def QuadraticMap.Anisotropic {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) :

                                              An anisotropic quadratic map is zero only on zero vectors.

                                              Equations
                                              • Q.Anisotropic = ∀ (x : M), Q x = 0x = 0
                                              Instances For
                                                theorem QuadraticMap.not_anisotropic_iff_exists {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) :
                                                ¬Q.Anisotropic ∃ (x : M), x 0 Q x = 0
                                                theorem QuadraticMap.Anisotropic.eq_zero_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {Q : QuadraticMap R M N} (h : Q.Anisotropic) {x : M} :
                                                Q x = 0 x = 0
                                                theorem QuadraticMap.separatingLeft_of_anisotropic {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticMap R M R) (hB : Q.Anisotropic) :
                                                LinearMap.SeparatingLeft (QuadraticMap.associated' Q)

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

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

                                                A positive definite quadratic form is positive on nonzero vectors.

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

                                                  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 (nR) R

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

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

                                                    A matrix representation of the quadratic form.

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

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

                                                      Equations
                                                      • Q.discr = Q.toMatrix'.det
                                                      Instances For
                                                        theorem QuadraticMap.discr_smul {R : Type u_3} {n : Type w} [Fintype n] [CommRing R] [DecidableEq n] [Invertible 2] {Q : QuadraticMap R (nR) 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 (nR) R} (f : (nR) →ₗ[R] nR) :
                                                        (Q.comp f).discr = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr

                                                        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 (Module.finrank K V)) K V), LinearMap.IsOrthoᵢ B v

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

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

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

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

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

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

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

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