# Quadratic form on product and pi types #

## Main definitions #

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

## Main results #

• quadratic_form.equivalent.prod, quadratic_form.equivalent.pi: quadratic forms are equivalent if their components are equivalent
• quadratic_form.nonneg_prod_iff, quadratic_form.nonneg_pi_iff: quadratic forms are positive- semidefinite if and only if their components are positive-semidefinite.
• quadratic_form.pos_def_prod_iff, quadratic_form.pos_def_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.

def quadratic_form.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [ring R] [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) :
(M₁ × M₂)

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

Equations
@[simp]
theorem quadratic_form.prod_to_fun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [ring R] [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) (ᾰ : M₁ × M₂) :
(Q₁.prod Q₂) = Q₁ ᾰ.fst + Q₂ ᾰ.snd
def quadratic_form.isometry.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [ring R] [add_comm_group M₁] [add_comm_group M₂] [add_comm_group N₁] [add_comm_group N₂] [ M₁] [ M₂] [ N₁] [ N₂] {Q₁ : M₁} {Q₂ : M₂} {Q₁' : N₁} {Q₂' : N₂} (e₁ : Q₁.isometry Q₁') (e₂ : Q₂.isometry Q₂') :
(Q₁.prod Q₂).isometry (Q₁'.prod Q₂')

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

Equations
@[simp]
theorem quadratic_form.isometry.prod_to_linear_equiv {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [ring R] [add_comm_group M₁] [add_comm_group M₂] [add_comm_group N₁] [add_comm_group N₂] [ M₁] [ M₂] [ N₁] [ N₂] {Q₁ : M₁} {Q₂ : M₂} {Q₁' : N₁} {Q₂' : N₂} (e₁ : Q₁.isometry Q₁') (e₂ : Q₂.isometry Q₂') :
(e₁.prod e₂).to_linear_equiv =
theorem quadratic_form.equivalent.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [ring R] [add_comm_group M₁] [add_comm_group M₂] [add_comm_group N₁] [add_comm_group N₂] [ M₁] [ M₂] [ N₁] [ N₂] {Q₁ : M₁} {Q₂ : M₂} {Q₁' : N₁} {Q₂' : N₂} (e₁ : Q₁.equivalent Q₁') (e₂ : Q₂.equivalent Q₂') :
(Q₁.prod Q₂).equivalent (Q₁'.prod Q₂')
theorem quadratic_form.anisotropic_of_prod {M₁ : Type u_3} {M₂ : Type u_4} [add_comm_group M₁] [add_comm_group M₂] {R : Type u_1} [ordered_ring R] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (h : (Q₁.prod Q₂).anisotropic) :

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

theorem quadratic_form.nonneg_prod_iff {M₁ : Type u_3} {M₂ : Type u_4} [add_comm_group M₁] [add_comm_group M₂] {R : Type u_1} [ordered_ring R] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} :
(∀ (x : M₁ × M₂), 0 (Q₁.prod Q₂) x) (∀ (x : M₁), 0 Q₁ x) ∀ (x : M₂), 0 Q₂ x
theorem quadratic_form.pos_def_prod_iff {M₁ : Type u_3} {M₂ : Type u_4} [add_comm_group M₁] [add_comm_group M₂] {R : Type u_1} [ordered_ring R] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} :
(Q₁.prod Q₂).pos_def Q₁.pos_def Q₂.pos_def
theorem quadratic_form.pos_def.prod {M₁ : Type u_3} {M₂ : Type u_4} [add_comm_group M₁] [add_comm_group M₂] {R : Type u_1} [ordered_ring R] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (h₁ : Q₁.pos_def) (h₂ : Q₂.pos_def) :
(Q₁.prod Q₂).pos_def
def quadratic_form.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [ring R] [Π (i : ι), add_comm_group (Mᵢ i)] [Π (i : ι), (Mᵢ i)] [fintype ι] (Q : Π (i : ι), (Mᵢ i)) :
(Π (i : ι), Mᵢ i)

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

Equations
@[simp]
theorem quadratic_form.pi_apply {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [ring R] [Π (i : ι), add_comm_group (Mᵢ i)] [Π (i : ι), (Mᵢ i)] [fintype ι] (Q : Π (i : ι), (Mᵢ i)) (x : Π (i : ι), Mᵢ i) :
x = finset.univ.sum (λ (i : ι), (Q i) (x i))
@[simp]
theorem quadratic_form.isometry.pi_to_linear_equiv {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} {Nᵢ : ι → Type u_8} [ring R] [Π (i : ι), add_comm_group (Mᵢ i)] [Π (i : ι), add_comm_group (Nᵢ i)] [Π (i : ι), (Mᵢ i)] [Π (i : ι), (Nᵢ i)] [fintype ι] {Q : Π (i : ι), (Mᵢ i)} {Q' : Π (i : ι), (Nᵢ i)} (e : Π (i : ι), (Q i).isometry (Q' i)) :
= linear_equiv.Pi_congr_right (λ (i : ι), (e i))
def quadratic_form.isometry.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} {Nᵢ : ι → Type u_8} [ring R] [Π (i : ι), add_comm_group (Mᵢ i)] [Π (i : ι), add_comm_group (Nᵢ i)] [Π (i : ι), (Mᵢ i)] [Π (i : ι), (Nᵢ i)] [fintype ι] {Q : Π (i : ι), (Mᵢ i)} {Q' : Π (i : ι), (Nᵢ i)} (e : Π (i : ι), (Q i).isometry (Q' i)) :

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

Equations
theorem quadratic_form.equivalent.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} {Nᵢ : ι → Type u_8} [ring R] [Π (i : ι), add_comm_group (Mᵢ i)] [Π (i : ι), add_comm_group (Nᵢ i)] [Π (i : ι), (Mᵢ i)] [Π (i : ι), (Nᵢ i)] [fintype ι] {Q : Π (i : ι), (Mᵢ i)} {Q' : Π (i : ι), (Nᵢ i)} (e : ∀ (i : ι), (Q i).equivalent (Q' i)) :
theorem quadratic_form.anisotropic_of_pi {ι : Type u_1} {Mᵢ : ι → Type u_7} [Π (i : ι), add_comm_group (Mᵢ i)] [fintype ι] {R : Type u_2} [ordered_ring R] [Π (i : ι), (Mᵢ i)] {Q : Π (i : ι), (Mᵢ i)} (h : .anisotropic) (i : ι) :

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

theorem quadratic_form.nonneg_pi_iff {ι : Type u_1} {Mᵢ : ι → Type u_7} [Π (i : ι), add_comm_group (Mᵢ i)] [fintype ι] {R : Type u_2} [ordered_ring R] [Π (i : ι), (Mᵢ i)] {Q : Π (i : ι), (Mᵢ i)} :
(∀ (x : Π (i : ι), (λ (i : ι), Mᵢ i) i), 0 x) ∀ (i : ι) (x : Mᵢ i), 0 (Q i) x
theorem quadratic_form.pos_def_pi_iff {ι : Type u_1} {Mᵢ : ι → Type u_7} [Π (i : ι), add_comm_group (Mᵢ i)] [fintype ι] {R : Type u_2} [ordered_ring R] [Π (i : ι), (Mᵢ i)] {Q : Π (i : ι), (Mᵢ i)} :
∀ (i : ι), (Q i).pos_def