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.

source

@[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

source

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

source

@[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

source

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₂') :

QuadraticForm.IsometryEquiv (QuadraticForm.prod Q₁ Q₂) (QuadraticForm.prod 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

source

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₂') :

QuadraticForm.Equivalent (QuadraticForm.prod Q₁ Q₂) (QuadraticForm.prod Q₁' Q₂')

source

@[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

source

@[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

source

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₂) :

QuadraticForm.IsometryEquiv (QuadraticForm.prod Q₁ Q₂) (QuadraticForm.prod Q₂ Q₁)

LinearEquiv.prodComm is isometric.

Instances For

source

@[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)

source

@[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)

source

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₂) :

QuadraticForm.IsometryEquiv (QuadraticForm.prod (QuadraticForm.prod Q₁ Q₂) (QuadraticForm.prod Q₃ Q₄)) (QuadraticForm.prod (QuadraticForm.prod Q₁ Q₃) (QuadraticForm.prod Q₂ Q₄))

LinearEquiv.prodProdProdComm is isometric.

Instances For

source

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₂)) :

QuadraticForm.Anisotropic Q₁ ∧ QuadraticForm.Anisotropic Q₂

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

source

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

source

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₂} :

QuadraticForm.PosDef (QuadraticForm.prod Q₁ Q₂) ↔ QuadraticForm.PosDef Q₁ ∧ QuadraticForm.PosDef Q₂

source

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₂) :

QuadraticForm.PosDef (QuadraticForm.prod Q₁ Q₂)

source

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

source

@[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)

source

@[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

source

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)) :

QuadraticForm.IsometryEquiv (QuadraticForm.pi Q) (QuadraticForm.pi Q')

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

source

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)) :

QuadraticForm.Equivalent (QuadraticForm.pi Q) (QuadraticForm.pi Q')

source

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

QuadraticForm.Anisotropic (Q i)

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

source

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

source

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

QuadraticForm.PosDef (QuadraticForm.pi Q) ↔ ∀ (i : ι), QuadraticForm.PosDef (Q i)