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

• Q₁.prod Q₂ = Q₁.comp (LinearMap.fst R M₁ M₂) + Q₂.comp (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₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') : (e₁.prod e₂).toLinearEquiv = e₁.prod 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₁ : 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.

Equations

• e₁.prod e₂ = { toLinearEquiv := e₁.prod e₂.toLinearEquiv, map_app' := ⋯ }

@[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₁.Isometry (Q₁.prod Q₂)

LinearMap.inl as an isometry.

Equations

• QuadraticForm.Isometry.inl Q₁ Q₂ = { toLinearMap := LinearMap.inl R M₁ M₂, map_app' := ⋯ }

@[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₂.Isometry (Q₁.prod Q₂)

LinearMap.inr as an isometry.

Equations

• QuadraticForm.Isometry.inr Q₁ Q₂ = { toLinearMap := LinearMap.inr R M₁ M₂, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.Isometry.fst_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₁) (self : M₁ × M₂) : (QuadraticForm.Isometry.fst M₂ Q₁) self = self.1

def QuadraticForm.Isometry.fst {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₁.prod 0).Isometry Q₁

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

Equations

• QuadraticForm.Isometry.fst M₂ Q₁ = { toLinearMap := LinearMap.fst R M₁ M₂, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.Isometry.snd_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₂) (self : M₁ × M₂) : (QuadraticForm.Isometry.snd M₁ Q₂) self = self.2

def QuadraticForm.Isometry.snd {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₂) : (QuadraticForm.prod 0 Q₂).Isometry Q₂

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

Equations

• QuadraticForm.Isometry.snd M₁ Q₂ = { toLinearMap := LinearMap.snd R M₁ M₂, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.Isometry.fst_comp_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₁) : (QuadraticForm.Isometry.fst M₂ Q₁).comp (QuadraticForm.Isometry.inl Q₁ 0) = QuadraticForm.Isometry.id Q₁

@[simp]

theorem QuadraticForm.Isometry.snd_comp_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₂) : (QuadraticForm.Isometry.snd M₁ Q₂).comp (QuadraticForm.Isometry.inr 0 Q₂) = QuadraticForm.Isometry.id Q₂

@[simp]

theorem QuadraticForm.Isometry.snd_comp_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₂) : (QuadraticForm.Isometry.snd M₁ Q₂).comp (QuadraticForm.Isometry.inl 0 Q₂) = 0

@[simp]

theorem QuadraticForm.Isometry.fst_comp_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₁) : (QuadraticForm.Isometry.fst M₂ Q₁).comp (QuadraticForm.Isometry.inr Q₁ 0) = 0

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₁ : Q₁.Equivalent Q₁') (e₂ : Q₂.Equivalent Q₂') : (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂')

@[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 = a.swap

@[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₂).invFun a = a.swap

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

LinearEquiv.prodComm is isometric.

Equations

• QuadraticForm.IsometryEquiv.prodComm Q₁ Q₂ = { toLinearEquiv := LinearEquiv.prodComm R M₁ M₂, map_app' := ⋯ }

@[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₄).invFun mmnn = ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2)

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

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

LinearEquiv.prodProdProdComm is isometric.

Equations

• QuadraticForm.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄ = { toLinearEquiv := LinearEquiv.prodProdProdComm R M₁ M₂ N₁ N₂, map_app' := ⋯ }

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 : (Q₁.prod Q₂).Anisotropic) : Q₁.Anisotropic ∧ Q₂.Anisotropic

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 ≤ (Q₁.prod 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₂} : (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

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₁ : Q₁.PosDef) (h₂ : Q₂.PosDef) : (Q₁.prod Q₂).PosDef

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₁ : Q₁.IsOrtho v.1 w.1) (h₂ : Q₂.IsOrtho v.2 w.2) : (Q₁.prod Q₂).IsOrtho 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₂) : (Q₁.prod Q₂).IsOrtho (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₂) : (Q₁.prod Q₂).IsOrtho (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₁) : (Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho 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₂) : (Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho 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 (⇑(Q₁.prod 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₂) : (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 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 (Q₁.prod Q₂) = LinearMap.compl₁₂ (QuadraticForm.associated Q₁) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ (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.univ.sum fun (i : ι) => (Q i).comp (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.univ.sum 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 : ι) → (Q i).IsometryEquiv (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 : ι) → (Q i).IsometryEquiv (Q' i)) : (QuadraticForm.pi Q).IsometryEquiv (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

• QuadraticForm.IsometryEquiv.pi e = { toLinearEquiv := LinearEquiv.piCongrRight fun (i : ι) => (e i).toLinearEquiv, map_app' := ⋯ }

@[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).Isometry (QuadraticForm.pi Q)

LinearMap.single as an isometry.

Equations

• QuadraticForm.Isometry.single Q i = { toLinearMap := LinearMap.single i, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.Isometry.proj_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 ι] (i : ι) (Q : QuadraticForm R (Mᵢ i)) (f : (x : ι) → (fun (i : ι) => Mᵢ i) x) : (QuadraticForm.Isometry.proj i Q) f = f i

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

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

Equations

• QuadraticForm.Isometry.proj i Q = { toLinearMap := LinearMap.proj i, map_app' := ⋯ }

@[simp]

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

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

@[simp]

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

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

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 : ι), (Q i).Equivalent (Q' i)) : (QuadraticForm.pi Q).Equivalent (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.pi Q).Anisotropic) (i : ι) : (Q i).Anisotropic

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.pi Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef

@[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.univ.sum 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.pi Q).polarBilin = Finset.univ.sum fun (i : ι) => LinearMap.compl₁₂ (Q i).polarBilin (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.univ.sum fun (i : ι) => LinearMap.compl₁₂ (QuadraticForm.associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)