Documentation

Mathlib.LinearAlgebra.QuadraticForm.Prod

Quadratic form on product and pi types #

Main definitions #

Main results #

Implementation notes #

Many of the lemmas in this file could be generalized into results about sums of positive and non-negative elements, and would generalize to any map Q where Q 0 = 0, not just quadratic forms specifically.

@[simp]
theorem QuadraticForm.prod_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (a : M₁ × M₂) :
↑(QuadraticForm.prod Q₁ Q₂) a = Q₁ a.fst + Q₂ a.snd
def QuadraticForm.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :
QuadraticForm R (M₁ × M₂)

Construct a quadratic form on a product of two modules from the quadratic form on each module.

Instances For
    @[simp]
    theorem QuadraticForm.IsometryEquiv.prod_toLinearEquiv {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} (e₁ : QuadraticForm.IsometryEquiv Q₁ Q₁') (e₂ : QuadraticForm.IsometryEquiv Q₂ Q₂') :
    (QuadraticForm.IsometryEquiv.prod e₁ e₂).toLinearEquiv = LinearEquiv.prod e₁.toLinearEquiv e₂.toLinearEquiv
    def QuadraticForm.IsometryEquiv.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} (e₁ : QuadraticForm.IsometryEquiv Q₁ Q₁') (e₂ : QuadraticForm.IsometryEquiv Q₂ Q₂') :

    An isometry between quadratic forms generated by QuadraticForm.prod can be constructed from a pair of isometries between the left and right parts.

    Instances For
      theorem QuadraticForm.Equivalent.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} (e₁ : QuadraticForm.Equivalent Q₁ Q₁') (e₂ : QuadraticForm.Equivalent Q₂ Q₂') :
      @[simp]
      theorem QuadraticForm.IsometryEquiv.prodComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :
      ∀ (a : M₁ × M₂), ↑(QuadraticForm.IsometryEquiv.prodComm Q₁ Q₂) a = Prod.swap a
      @[simp]
      theorem QuadraticForm.IsometryEquiv.prodComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :
      ∀ (a : M₂ × M₁), LinearEquiv.invFun (QuadraticForm.IsometryEquiv.prodComm Q₁ Q₂).toLinearEquiv a = Prod.swap a
      def QuadraticForm.IsometryEquiv.prodComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :

      LinearEquiv.prodComm is isometric.

      Instances For
        @[simp]
        theorem QuadraticForm.IsometryEquiv.prodProdProdComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R N₁) (Q₄ : QuadraticForm R N₂) (mnmn : (M₁ × M₂) × N₁ × N₂) :
        ↑(QuadraticForm.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄) mnmn = ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd)
        @[simp]
        theorem QuadraticForm.IsometryEquiv.prodProdProdComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R N₁) (Q₄ : QuadraticForm R N₂) (mmnn : (M₁ × N₁) × M₂ × N₂) :
        LinearEquiv.invFun (QuadraticForm.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄).toLinearEquiv mmnn = ((mmnn.fst.fst, mmnn.snd.fst), mmnn.fst.snd, mmnn.snd.snd)
        def QuadraticForm.IsometryEquiv.prodProdProdComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R N₁) (Q₄ : QuadraticForm R N₂) :

        LinearEquiv.prodProdProdComm is isometric.

        Instances For
          theorem QuadraticForm.anisotropic_of_prod {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedRing R] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : QuadraticForm.Anisotropic (QuadraticForm.prod Q₁ Q₂)) :

          If a product is anisotropic then its components must be. The converse is not true.

          theorem QuadraticForm.nonneg_prod_iff {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedRing R] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} :
          (∀ (x : M₁ × M₂), 0 ↑(QuadraticForm.prod Q₁ Q₂) x) (∀ (x : M₁), 0 Q₁ x) ∀ (x : M₂), 0 Q₂ x
          theorem QuadraticForm.posDef_prod_iff {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedRing R] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} :
          theorem QuadraticForm.PosDef.prod {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedRing R] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h₁ : QuadraticForm.PosDef Q₁) (h₂ : QuadraticForm.PosDef Q₂) :
          def QuadraticForm.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_7} [Semiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) :
          QuadraticForm R ((i : ι) → Mᵢ i)

          Construct a quadratic form on a family of modules from the quadratic form on each module.

          Instances For
            @[simp]
            theorem QuadraticForm.pi_apply {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_7} [Semiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) (x : (i : ι) → Mᵢ i) :
            ↑(QuadraticForm.pi Q) x = Finset.sum Finset.univ fun i => ↑(Q i) (x i)
            @[simp]
            theorem QuadraticForm.IsometryEquiv.pi_toLinearEquiv {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_7} {Nᵢ : ιType u_8} [Semiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Fintype ι] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} {Q' : (i : ι) → QuadraticForm R (Nᵢ i)} (e : (i : ι) → QuadraticForm.IsometryEquiv (Q i) (Q' i)) :
            (QuadraticForm.IsometryEquiv.pi e).toLinearEquiv = LinearEquiv.piCongrRight fun i => (e i).toLinearEquiv
            def QuadraticForm.IsometryEquiv.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_7} {Nᵢ : ιType u_8} [Semiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Fintype ι] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} {Q' : (i : ι) → QuadraticForm R (Nᵢ i)} (e : (i : ι) → QuadraticForm.IsometryEquiv (Q i) (Q' i)) :

            An isometry between quadratic forms generated by QuadraticForm.pi can be constructed from a pair of isometries between the left and right parts.

            Instances For
              theorem QuadraticForm.Equivalent.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_7} {Nᵢ : ιType u_8} [Semiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Fintype ι] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} {Q' : (i : ι) → QuadraticForm R (Nᵢ i)} (e : ∀ (i : ι), QuadraticForm.Equivalent (Q i) (Q' i)) :
              theorem QuadraticForm.anisotropic_of_pi {ι : Type u_1} {Mᵢ : ιType u_7} [(i : ι) → AddCommMonoid (Mᵢ i)] [Fintype ι] {R : Type u_9} [OrderedRing R] [(i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} (h : QuadraticForm.Anisotropic (QuadraticForm.pi Q)) (i : ι) :

              If a family is anisotropic then its components must be. The converse is not true.

              theorem QuadraticForm.nonneg_pi_iff {ι : Type u_1} {Mᵢ : ιType u_7} [(i : ι) → AddCommMonoid (Mᵢ i)] [Fintype ι] {R : Type u_9} [OrderedRing R] [(i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} :
              (∀ (x : (i : ι) → Mᵢ i), 0 ↑(QuadraticForm.pi Q) x) ∀ (i : ι) (x : Mᵢ i), 0 ↑(Q i) x
              theorem QuadraticForm.posDef_pi_iff {ι : Type u_1} {Mᵢ : ιType u_7} [(i : ι) → AddCommMonoid (Mᵢ i)] [Fintype ι] {R : Type u_9} [OrderedRing R] [(i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} :