# Quadratic form on product and pi types #

## Main definitions #

• QuadraticForm.prod Q₁ Q₂: the quadratic form constructed elementwise on a product
• QuadraticForm.pi Q: the quadratic form constructed elementwise on a pi type

## Main results #

• QuadraticForm.Equivalent.prod, QuadraticForm.Equivalent.pi: quadratic forms are equivalent if their components are equivalent
• QuadraticForm.nonneg_prod_iff, QuadraticForm.nonneg_pi_iff: quadratic forms are positive- semidefinite if and only if their components are positive-semidefinite.
• QuadraticForm.posDef_prod_iff, QuadraticForm.posDef_pi_iff: quadratic forms are positive- definite if and only if their components are positive-definite.

## 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} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) (a : M₁ × M₂) :
↑() a = Q₁ a.fst + Q₂ a.snd
def QuadraticForm.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) :

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} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] {Q₁ : } {Q₂ : } {Q₁' : } {Q₂' : } (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} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] {Q₁ : } {Q₂ : } {Q₁' : } {Q₂' : } (e₁ : ) (e₂ : ) :

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} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] {Q₁ : } {Q₂ : } {Q₁' : } {Q₂' : } (e₁ : ) (e₂ : ) :
@[simp]
theorem QuadraticForm.IsometryEquiv.prodComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) :
∀ (a : M₁ × M₂), ↑() a =
@[simp]
theorem QuadraticForm.IsometryEquiv.prodComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) :
∀ (a : M₂ × M₁), LinearEquiv.invFun ().toLinearEquiv a =
def QuadraticForm.IsometryEquiv.prodComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) :

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} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (Q₁ : ) (Q₂ : ) (Q₃ : ) (Q₄ : ) (mnmn : (M₁ × M₂) × N₁ × N₂) :
↑() 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} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (Q₁ : ) (Q₂ : ) (Q₃ : ) (Q₄ : ) (mmnn : (M₁ × N₁) × M₂ × N₂) :
LinearEquiv.invFun ().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} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (Q₁ : ) (Q₂ : ) (Q₃ : ) (Q₄ : ) :

LinearEquiv.prodProdProdComm is isometric.

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

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} [] [] {R : Type u_9} [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } :
(∀ (x : M₁ × M₂), 0 ↑() x) (∀ (x : M₁), 0 Q₁ x) ∀ (x : M₂), 0 Q₂ x
theorem QuadraticForm.posDef_prod_iff {M₁ : Type u_3} {M₂ : Type u_4} [] [] {R : Type u_9} [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } :
theorem QuadraticForm.PosDef.prod {M₁ : Type u_3} {M₂ : Type u_4} [] [] {R : Type u_9} [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (h₁ : ) (h₂ : ) :
def QuadraticForm.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ιType u_7} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [] (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} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) (x : (i : ι) → Mᵢ i) :
↑() 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} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} {Q' : (i : ι) → QuadraticForm R (Nᵢ i)} (e : (i : ι) → QuadraticForm.IsometryEquiv (Q i) (Q' i)) :
().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} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [] {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} [] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [] {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)] [] {R : Type u_9} [] [(i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} (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)] [] {R : Type u_9} [] [(i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} :
(∀ (x : (i : ι) → Mᵢ i), 0 ↑() 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)] [] {R : Type u_9} [] [(i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} :
∀ (i : ι), QuadraticForm.PosDef (Q i)