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.

def QuadraticMap.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) : QuadraticMap R (M₁ × M₂) P

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

@[simp]

theorem QuadraticMap.prod_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (a : M₁ × M₂) : (Q₁.prod Q₂) a = Q₁ a.1 + Q₂ a.2

def QuadraticMap.IsometryEquiv.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P} {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') : (Q₁.prod Q₂).IsometryEquiv (Q₁'.prod Q₂')

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

@[simp]

theorem QuadraticMap.IsometryEquiv.prod_toLinearEquiv {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P} {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') : (e₁.prod e₂).toLinearEquiv = e₁.prodCongr e₂.toLinearEquiv

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

LinearMap.inl as an isometry.

@[simp]

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

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

LinearMap.inr as an isometry.

@[simp]

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

def QuadraticMap.Isometry.fst {R : Type u_2} {M₁ : Type u_3} (M₂ : Type u_4) {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) : Q₁.prod 0 →qᵢ Q₁

LinearMap.fst as an isometry, when the second space has the zero quadratic form.

@[simp]

theorem QuadraticMap.Isometry.fst_apply {R : Type u_2} {M₁ : Type u_3} (M₂ : Type u_4) {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (self : M₁ × M₂) : (fst M₂ Q₁) self = self.1

def QuadraticMap.Isometry.snd {R : Type u_2} (M₁ : Type u_3) {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) : prod 0 Q₂ →qᵢ Q₂

LinearMap.snd as an isometry, when the first space has the zero quadratic form.

@[simp]

theorem QuadraticMap.Isometry.snd_apply {R : Type u_2} (M₁ : Type u_3) {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) (self : M₁ × M₂) : (snd M₁ Q₂) self = self.2

@[simp]

theorem QuadraticMap.Isometry.fst_comp_inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) : (fst M₂ Q₁).comp (inl Q₁ 0) = id Q₁

@[simp]

theorem QuadraticMap.Isometry.snd_comp_inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) : (snd M₁ Q₂).comp (inr 0 Q₂) = id Q₂

@[simp]

theorem QuadraticMap.Isometry.snd_comp_inl {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₂ : QuadraticMap R M₂ P) : (snd M₁ Q₂).comp (inl 0 Q₂) = 0

@[simp]

theorem QuadraticMap.Isometry.fst_comp_inr {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) : (fst M₂ Q₁).comp (inr Q₁ 0) = 0

theorem QuadraticMap.Equivalent.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P} {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.Equivalent Q₁') (e₂ : Q₂.Equivalent Q₂') : (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂')

def QuadraticMap.IsometryEquiv.prodComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) : (Q₁.prod Q₂).IsometryEquiv (Q₂.prod Q₁)

LinearEquiv.prodComm is isometric.

@[simp]

theorem QuadraticMap.IsometryEquiv.prodComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (a✝ : M₁ × M₂) : (prodComm Q₁ Q₂) a✝ = a✝.swap

@[simp]

theorem QuadraticMap.IsometryEquiv.prodComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (a✝ : M₂ × M₁) : (prodComm Q₁ Q₂).invFun a✝ = a✝.swap

def QuadraticMap.IsometryEquiv.prodProdProdComm {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P) (Q₄ : QuadraticMap R N₂ P) : ((Q₁.prod Q₂).prod (Q₃.prod Q₄)).IsometryEquiv ((Q₁.prod Q₃).prod (Q₂.prod Q₄))

LinearEquiv.prodProdProdComm is isometric.

@[simp]

theorem QuadraticMap.IsometryEquiv.prodProdProdComm_invFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P) (Q₄ : QuadraticMap R N₂ P) (mmnn : (M₁ × N₁) × M₂ × N₂) : (prodProdProdComm Q₁ Q₂ Q₃ Q₄).invFun mmnn = ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2)

@[simp]

theorem QuadraticMap.IsometryEquiv.prodProdProdComm_toFun {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P) (Q₄ : QuadraticMap R N₂ P) (mnmn : (M₁ × M₂) × N₁ × N₂) : (prodProdProdComm Q₁ Q₂ Q₃ Q₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)

theorem QuadraticMap.anisotropic_of_prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (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 QuadraticMap.nonneg_prod_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] [Preorder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} : (∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x

theorem QuadraticMap.posDef_prod_iff {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] [PartialOrder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} : (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

theorem QuadraticMap.PosDef.prod {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] [PartialOrder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (h₁ : Q₁.PosDef) (h₂ : Q₂.PosDef) : (Q₁.prod Q₂).PosDef

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def QuadraticMap.pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) : QuadraticMap R ((i : ι) → Mᵢ i) P

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

@[simp]

theorem QuadraticMap.pi_apply {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (x : (i : ι) → Mᵢ i) : (pi Q) x = ∑ i : ι, (Q i) (x i)

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

def QuadraticMap.IsometryEquiv.pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} {Nᵢ : ι → Type u_9} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Module R P] [Fintype ι] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} (e : (i : ι) → (Q i).IsometryEquiv (Q' i)) : (QuadraticMap.pi Q).IsometryEquiv (QuadraticMap.pi Q')

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

@[simp]

theorem QuadraticMap.IsometryEquiv.pi_toLinearEquiv {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} {Nᵢ : ι → Type u_9} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Module R P] [Fintype ι] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} (e : (i : ι) → (Q i).IsometryEquiv (Q' i)) : (pi e).toLinearEquiv = LinearEquiv.piCongrRight fun (i : ι) => (e i).toLinearEquiv

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

LinearMap.single as an isometry.

@[simp]

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

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

LinearMap.proj as an isometry, when all but one quadratic form is zero.

@[simp]

theorem QuadraticMap.Isometry.proj_apply {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] [DecidableEq ι] (i : ι) (Q : QuadraticMap R (Mᵢ i) P) (f : (x : ι) → Mᵢ x) : (proj i Q) f = f i

@[simp]

theorem QuadraticMap.Isometry.proj_comp_single_of_same {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] [DecidableEq ι] (i : ι) (Q : QuadraticMap R (Mᵢ i) P) : (proj i Q).comp (single (Pi.single i Q) i) = ofEq ⋯

Note that QuadraticMap.Isometry.id would not be well-typed as the RHS.

@[simp]

theorem QuadraticMap.Isometry.proj_comp_single_of_ne {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] [DecidableEq ι] {i j : ι} (h : i ≠ j) (Q : QuadraticMap R (Mᵢ i) P) : (proj i Q).comp (single (Pi.single i Q) j) = comp 0 (ofEq ⋯)

Note that 0 : 0 →qᵢ Q alone would not be well-typed as the RHS.

theorem QuadraticMap.Equivalent.pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} {Nᵢ : ι → Type u_9} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → AddCommMonoid (Nᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [(i : ι) → Module R (Nᵢ i)] [Module R P] [Fintype ι] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} (e : ∀ (i : ι), (Q i).Equivalent (Q' i)) : (QuadraticMap.pi Q).Equivalent (QuadraticMap.pi Q')

theorem QuadraticMap.anisotropic_of_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [AddCommMonoid P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} (h : (pi Q).Anisotropic) (i : ι) : (Q i).Anisotropic

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

theorem QuadraticMap.nonneg_pi_iff {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] {P : Type u_10} [Fintype ι] [AddCommMonoid P] [PartialOrder P] [IsOrderedAddMonoid P] [Module R P] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} : (∀ (x : (i : ι) → Mᵢ i), 0 ≤ (pi Q) x) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

theorem QuadraticMap.posDef_pi_iff {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_8} [CommSemiring R] [(i : ι) → AddCommMonoid (Mᵢ i)] [(i : ι) → Module R (Mᵢ i)] {P : Type u_10} [Fintype ι] [AddCommMonoid P] [PartialOrder P] [IsOrderedAddMonoid P] [Module R P] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} : (pi Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef

@[simp]

theorem QuadraticMap.Ring.polar_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommRing R] [(i : ι) → AddCommGroup (Mᵢ i)] [AddCommGroup P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (x y : (i : ι) → Mᵢ i) : polar (⇑(pi Q)) x y = ∑ i : ι, polar (⇑(Q i)) (x i) (y i)

@[simp]

theorem QuadraticMap.Ring.polarBilin_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommRing R] [(i : ι) → AddCommGroup (Mᵢ i)] [AddCommGroup P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) : (pi Q).polarBilin = ∑ i : ι, LinearMap.compl₁₂ (Q i).polarBilin (LinearMap.proj i) (LinearMap.proj i)

@[simp]

theorem QuadraticMap.Ring.associated_pi {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [CommRing R] [(i : ι) → AddCommGroup (Mᵢ i)] [AddCommGroup P] [(i : ι) → Module R (Mᵢ i)] [Module R P] [Fintype ι] [Invertible 2] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) : associated (pi Q) = ∑ i : ι, LinearMap.compl₁₂ (associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)