Quadratic form on product and pi types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
quadratic_form.prod Q₁ Q₂: the quadratic form constructed elementwise on a productquadratic_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 equivalentquadratic_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.
@[simp]
theorem
quadratic_form.prod_apply
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂)
(ᾰ : M₁ × M₂) :
def
quadratic_form.prod
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂) :
quadratic_form R (M₁ × M₂)
Construct a quadratic form on a product of two modules from the quadratic form on each module.
Equations
- Q₁.prod Q₂ = Q₁.comp (linear_map.fst R M₁ M₂) + Q₂.comp (linear_map.snd R M₁ M₂)
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}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₁' : quadratic_form R N₁}
{Q₂' : quadratic_form R N₂}
(e₁ : Q₁.isometry Q₁')
(e₂ : Q₂.isometry 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
- e₁.prod e₂ = {to_linear_equiv := e₁.to_linear_equiv.prod e₂.to_linear_equiv, map_app' := _}
@[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}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₁' : quadratic_form R N₁}
{Q₂' : quadratic_form R N₂}
(e₁ : Q₁.isometry Q₁')
(e₂ : Q₂.isometry Q₂') :
(e₁.prod e₂).to_linear_equiv = e₁.to_linear_equiv.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}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₁' : quadratic_form R N₁}
{Q₂' : quadratic_form R 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_monoid M₁]
[add_comm_monoid M₂]
{R : Type u_1}
[ordered_ring R]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(h : (Q₁.prod Q₂).anisotropic) :
Q₁.anisotropic ∧ 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_monoid M₁]
[add_comm_monoid M₂]
{R : Type u_1}
[ordered_ring R]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
theorem
quadratic_form.pos_def_prod_iff
{M₁ : Type u_3}
{M₂ : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
{R : Type u_1}
[ordered_ring R]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
theorem
quadratic_form.pos_def.prod
{M₁ : Type u_3}
{M₂ : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
{R : Type u_1}
[ordered_ring R]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(h₁ : Q₁.pos_def)
(h₂ : Q₂.pos_def) :
def
quadratic_form.pi
{ι : Type u_1}
{R : Type u_2}
{Mᵢ : ι → Type u_7}
[semiring R]
[Π (i : ι), add_comm_monoid (Mᵢ i)]
[Π (i : ι), module R (Mᵢ i)]
[fintype ι]
(Q : Π (i : ι), quadratic_form R (Mᵢ i)) :
quadratic_form R (Π (i : ι), Mᵢ i)
Construct a quadratic form on a family of modules from the quadratic form on each module.
Equations
- quadratic_form.pi Q = finset.univ.sum (λ (i : ι), (Q i).comp (linear_map.proj i))
@[simp]
theorem
quadratic_form.pi_apply
{ι : Type u_1}
{R : Type u_2}
{Mᵢ : ι → Type u_7}
[semiring R]
[Π (i : ι), add_comm_monoid (Mᵢ i)]
[Π (i : ι), module R (Mᵢ i)]
[fintype ι]
(Q : Π (i : ι), quadratic_form R (Mᵢ i))
(x : Π (i : ι), Mᵢ i) :
⇑(quadratic_form.pi Q) 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}
[semiring R]
[Π (i : ι), add_comm_monoid (Mᵢ i)]
[Π (i : ι), add_comm_monoid (Nᵢ i)]
[Π (i : ι), module R (Mᵢ i)]
[Π (i : ι), module R (Nᵢ i)]
[fintype ι]
{Q : Π (i : ι), quadratic_form R (Mᵢ i)}
{Q' : Π (i : ι), quadratic_form R (Nᵢ i)}
(e : Π (i : ι), (Q i).isometry (Q' i)) :
(quadratic_form.isometry.pi e).to_linear_equiv = 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}
[semiring R]
[Π (i : ι), add_comm_monoid (Mᵢ i)]
[Π (i : ι), add_comm_monoid (Nᵢ i)]
[Π (i : ι), module R (Mᵢ i)]
[Π (i : ι), module R (Nᵢ i)]
[fintype ι]
{Q : Π (i : ι), quadratic_form R (Mᵢ i)}
{Q' : Π (i : ι), quadratic_form R (Nᵢ i)}
(e : Π (i : ι), (Q i).isometry (Q' i)) :
(quadratic_form.pi Q).isometry (quadratic_form.pi 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
- quadratic_form.isometry.pi e = {to_linear_equiv := linear_equiv.Pi_congr_right (λ (i : ι), ↑(e i)), map_app' := _}
theorem
quadratic_form.equivalent.pi
{ι : Type u_1}
{R : Type u_2}
{Mᵢ : ι → Type u_7}
{Nᵢ : ι → Type u_8}
[semiring R]
[Π (i : ι), add_comm_monoid (Mᵢ i)]
[Π (i : ι), add_comm_monoid (Nᵢ i)]
[Π (i : ι), module R (Mᵢ i)]
[Π (i : ι), module R (Nᵢ i)]
[fintype ι]
{Q : Π (i : ι), quadratic_form R (Mᵢ i)}
{Q' : Π (i : ι), quadratic_form R (Nᵢ i)}
(e : ∀ (i : ι), (Q i).equivalent (Q' i)) :
(quadratic_form.pi Q).equivalent (quadratic_form.pi Q')
theorem
quadratic_form.anisotropic_of_pi
{ι : Type u_1}
{Mᵢ : ι → Type u_7}
[Π (i : ι), add_comm_monoid (Mᵢ i)]
[fintype ι]
{R : Type u_2}
[ordered_ring R]
[Π (i : ι), module R (Mᵢ i)]
{Q : Π (i : ι), quadratic_form R (Mᵢ i)}
(h : (quadratic_form.pi Q).anisotropic)
(i : ι) :
(Q i).anisotropic
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_monoid (Mᵢ i)]
[fintype ι]
{R : Type u_2}
[ordered_ring R]
[Π (i : ι), module R (Mᵢ i)]
{Q : Π (i : ι), quadratic_form R (Mᵢ i)} :
theorem
quadratic_form.pos_def_pi_iff
{ι : Type u_1}
{Mᵢ : ι → Type u_7}
[Π (i : ι), add_comm_monoid (Mᵢ i)]
[fintype ι]
{R : Type u_2}
[ordered_ring R]
[Π (i : ι), module R (Mᵢ i)]
{Q : Π (i : ι), quadratic_form R (Mᵢ i)} :
(quadratic_form.pi Q).pos_def ↔ ∀ (i : ι), (Q i).pos_def