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} [CommSemiring 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.1 + Q₂ a.2

def QuadraticForm.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring 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.

Equations

• QuadraticForm.prod Q₁ Q₂ = QuadraticForm.comp Q₁ (LinearMap.fst R M₁ M₂) + QuadraticForm.comp Q₂ (LinearMap.snd R M₁ M₂)

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

def QuadraticForm.IsometryEquiv.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuadraticForm.Isometry.inl_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (i : M₁) : (QuadraticForm.Isometry.inl Q₁ Q₂) i = (i, 0)

def QuadraticForm.Isometry.inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Q₁ →qᵢ QuadraticForm.prod Q₁ Q₂

LinearMap.inl as an isometry.

Equations

• QuadraticForm.Isometry.inl Q₁ Q₂ = { toLinearMap := LinearMap.inl R M₁ M₂, map_app' := (_ : ∀ (m₁ : M₁), Q₁ m₁ + Q₂ 0 = Q₁ m₁) }

@[simp]

theorem QuadraticForm.Isometry.inr_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (i : M₂) : (QuadraticForm.Isometry.inr Q₁ Q₂) i = (0, i)

def QuadraticForm.Isometry.inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Q₂ →qᵢ QuadraticForm.prod Q₁ Q₂

LinearMap.inr as an isometry.

Equations

• QuadraticForm.Isometry.inr Q₁ Q₂ = { toLinearMap := LinearMap.inr R M₁ M₂, map_app' := (_ : ∀ (m₁ : M₂), Q₁ 0 + Q₂ m₁ = Q₂ m₁) }

theorem QuadraticForm.Equivalent.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring 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₂')

@[simp]

theorem QuadraticForm.IsometryEquiv.prodComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring 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₂).toLinearEquiv.invFun a = Prod.swap a

@[simp]

theorem QuadraticForm.IsometryEquiv.prodComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring 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

def QuadraticForm.IsometryEquiv.prodComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring 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.

Equations

• One or more equations did not get rendered due to their size.

@[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} [CommSemiring 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.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)

@[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} [CommSemiring 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₂) : (QuadraticForm.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄).toLinearEquiv.invFun mmnn = ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2)

def QuadraticForm.IsometryEquiv.prodProdProdComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring 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.

Equations

• One or more equations did not get rendered due to their size.

theorem QuadraticForm.anisotropic_of_prod {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedCommRing 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.

theorem QuadraticForm.nonneg_prod_iff {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedCommRing 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

theorem QuadraticForm.posDef_prod_iff {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedCommRing 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₂

theorem QuadraticForm.PosDef.prod {M₁ : Type u_3} {M₂ : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] {R : Type u_9} [OrderedCommRing 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₂)

theorem QuadraticForm.IsOrtho.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {v : M₁ × M₂} {w : M₁ × M₂} (h₁ : QuadraticForm.IsOrtho Q₁ v.1 w.1) (h₂ : QuadraticForm.IsOrtho Q₂ v.2 w.2) : QuadraticForm.IsOrtho (QuadraticForm.prod Q₁ Q₂) v w

@[simp]

theorem QuadraticForm.IsOrtho.inl_inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (m₁ : M₁) (m₂ : M₂) : QuadraticForm.IsOrtho (QuadraticForm.prod Q₁ Q₂) (m₁, 0) (0, m₂)

@[simp]

theorem QuadraticForm.IsOrtho.inr_inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (m₁ : M₁) (m₂ : M₂) : QuadraticForm.IsOrtho (QuadraticForm.prod Q₁ Q₂) (0, m₂) (m₁, 0)

@[simp]

theorem QuadraticForm.isOrtho_inl_inl_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (m₁ : M₁) (m₁' : M₁) : QuadraticForm.IsOrtho (QuadraticForm.prod Q₁ Q₂) (m₁, 0) (m₁', 0) ↔ QuadraticForm.IsOrtho Q₁ m₁ m₁'

@[simp]

theorem QuadraticForm.isOrtho_inr_inr_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (m₂ : M₂) (m₂' : M₂) : QuadraticForm.IsOrtho (QuadraticForm.prod Q₁ Q₂) (0, m₂) (0, m₂') ↔ QuadraticForm.IsOrtho Q₂ m₂ m₂'

@[simp]

theorem QuadraticForm.polar_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (x : M₁ × M₂) (y : M₁ × M₂) : QuadraticForm.polar (⇑(QuadraticForm.prod Q₁ Q₂)) x y = QuadraticForm.polar (⇑Q₁) x.1 y.1 + QuadraticForm.polar (⇑Q₂) x.2 y.2

@[simp]

theorem QuadraticForm.polarBilin_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm.polarBilin (QuadraticForm.prod Q₁ Q₂) = BilinForm.comp (QuadraticForm.polarBilin Q₁) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + BilinForm.comp (QuadraticForm.polarBilin Q₂) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)

@[simp]

theorem QuadraticForm.associated_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm.associated (QuadraticForm.prod Q₁ Q₂) = BilinForm.comp (QuadraticForm.associated Q₁) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + BilinForm.comp (QuadraticForm.associated Q₂) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)

def QuadraticForm.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommSemiring 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.

Equations

• QuadraticForm.pi Q = Finset.sum Finset.univ fun (i : ι) => QuadraticForm.comp (Q i) (LinearMap.proj i)

@[simp]

theorem QuadraticForm.pi_apply {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommSemiring 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)

theorem QuadraticForm.pi_apply_single {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] [DecidableEq ι] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) (i : ι) (m : Mᵢ i) : (QuadraticForm.pi Q) (Pi.single i m) = (Q i) m

@[simp]

theorem QuadraticForm.IsometryEquiv.pi_toLinearEquiv {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} {Nᵢ : ι → Type u_8} [CommSemiring 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

def QuadraticForm.IsometryEquiv.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} {Nᵢ : ι → Type u_8} [CommSemiring 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuadraticForm.Isometry.single_apply {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] [DecidableEq ι] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) (i : ι) (x : Mᵢ i) (j : ι) : (QuadraticForm.Isometry.single Q i) x j = Pi.single i x j

def QuadraticForm.Isometry.single {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] [DecidableEq ι] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) (i : ι) : Q i →qᵢ QuadraticForm.pi Q

LinearMap.single as an isometry.

Equations

• QuadraticForm.Isometry.single Q i = { toLinearMap := LinearMap.single i, map_app' := (_ : ∀ (m : Mᵢ i), (QuadraticForm.pi Q) (Pi.single i m) = (Q i) m) }

theorem QuadraticForm.Equivalent.pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} {Nᵢ : ι → Type u_8} [CommSemiring 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')

theorem QuadraticForm.anisotropic_of_pi {ι : Type u_1} {Mᵢ : ι → Type u_7} [(i : ι) → AddCommMonoid (Mᵢ i)] [Fintype ι] {R : Type u_9} [OrderedCommRing 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.

theorem QuadraticForm.nonneg_pi_iff {ι : Type u_1} {Mᵢ : ι → Type u_7} [(i : ι) → AddCommMonoid (Mᵢ i)] [Fintype ι] {R : Type u_9} [OrderedCommRing 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

theorem QuadraticForm.posDef_pi_iff {ι : Type u_1} {Mᵢ : ι → Type u_7} [(i : ι) → AddCommMonoid (Mᵢ i)] [Fintype ι] {R : Type u_9} [OrderedCommRing R] [(i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)} : QuadraticForm.PosDef (QuadraticForm.pi Q) ↔ ∀ (i : ι), QuadraticForm.PosDef (Q i)

@[simp]

theorem QuadraticForm.Ring.polar_pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommRing R] [(i : ι) → AddCommGroup (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) (x : (i : ι) → Mᵢ i) (y : (i : ι) → Mᵢ i) : QuadraticForm.polar (⇑(QuadraticForm.pi Q)) x y = Finset.sum Finset.univ fun (i : ι) => QuadraticForm.polar (⇑(Q i)) (x i) (y i)

@[simp]

theorem QuadraticForm.Ring.polarBilin_pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommRing R] [(i : ι) → AddCommGroup (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) : QuadraticForm.polarBilin (QuadraticForm.pi Q) = Finset.sum Finset.univ fun (i : ι) => BilinForm.comp (QuadraticForm.polarBilin (Q i)) (LinearMap.proj i) (LinearMap.proj i)

@[simp]

theorem QuadraticForm.Ring.associated_pi {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [CommRing R] [(i : ι) → AddCommGroup (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] [Fintype ι] [Invertible 2] (Q : (i : ι) → QuadraticForm R (Mᵢ i)) : QuadraticForm.associated (QuadraticForm.pi Q) = Finset.sum Finset.univ fun (i : ι) => BilinForm.comp (QuadraticForm.associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)