mathlib documentation

linear_algebra.quadratic_form.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 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₂) :
(Q₁.prod Q₂) = Q₁ ᾰ.fst + Q₂ ᾰ.snd
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
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₂') :
(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} [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₂') :
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) :

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₂} :
(∀ (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_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₂} :
(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_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) :
(Q₁.prod 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
@[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)) :
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)) :

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} [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)) :
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 : ι) :

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)} :
(∀ (x : Π (i : ι), (λ (i : ι), Mᵢ i) i), 0 (quadratic_form.pi Q) 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_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