Quadratic form on product and pi types #
Main definitions #
QuadraticForm.prod Q₁ Q₂: the quadratic form constructed elementwise on a productQuadraticForm.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 equivalentQuadraticForm.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
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₂)
:
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.
Equations
- Q₁.prod Q₂ = Q₁.comp (LinearMap.fst R M₁ M₂) + Q₂.comp (LinearMap.snd R M₁ M₂)
Instances For
@[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₁.prod e₂.toLinearEquiv
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.
Equations
- e₁.prod e₂ = { toLinearEquiv := e₁.prod e₂.toLinearEquiv, map_app' := ⋯ }
Instances For
@[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₁)
:
(QuadraticMap.Isometry.inl Q₁ Q₂) i = (i, 0)
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.
Equations
- QuadraticMap.Isometry.inl Q₁ Q₂ = { toLinearMap := LinearMap.inl R M₁ M₂, map_app' := ⋯ }
Instances For
@[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₂)
:
(QuadraticMap.Isometry.inr Q₁ Q₂) i = (0, i)
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.
Equations
- QuadraticMap.Isometry.inr Q₁ Q₂ = { toLinearMap := LinearMap.inr R M₁ M₂, map_app' := ⋯ }
Instances For
@[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₂)
:
(QuadraticMap.Isometry.fst M₂ Q₁) self = self.1
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.
Equations
- QuadraticMap.Isometry.fst M₂ Q₁ = { toLinearMap := LinearMap.fst R M₁ M₂, map_app' := ⋯ }
Instances For
@[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₂)
:
(QuadraticMap.Isometry.snd M₁ Q₂) self = self.2
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)
:
QuadraticMap.prod 0 Q₂ →qᵢ Q₂
LinearMap.snd as an isometry, when the first space has the zero quadratic form.
Equations
- QuadraticMap.Isometry.snd M₁ Q₂ = { toLinearMap := LinearMap.snd R M₁ M₂, map_app' := ⋯ }
Instances For
@[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)
:
(QuadraticMap.Isometry.fst M₂ Q₁).comp (QuadraticMap.Isometry.inl Q₁ 0) = QuadraticMap.Isometry.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)
:
(QuadraticMap.Isometry.snd M₁ Q₂).comp (QuadraticMap.Isometry.inr 0 Q₂) = QuadraticMap.Isometry.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)
:
(QuadraticMap.Isometry.snd M₁ Q₂).comp (QuadraticMap.Isometry.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)
:
(QuadraticMap.Isometry.fst M₂ Q₁).comp (QuadraticMap.Isometry.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₂')
@[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₁), (QuadraticMap.IsometryEquiv.prodComm Q₁ Q₂).invFun a = a.swap
@[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₂), (QuadraticMap.IsometryEquiv.prodComm Q₁ Q₂) a = a.swap
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.
Equations
- QuadraticMap.IsometryEquiv.prodComm Q₁ Q₂ = { toLinearEquiv := LinearEquiv.prodComm R M₁ M₂, map_app' := ⋯ }
Instances For
@[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₂)
:
(QuadraticMap.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
@[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₂)
:
(QuadraticMap.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄).invFun mmnn = ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2)
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.
Equations
- QuadraticMap.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄ = { toLinearEquiv := LinearEquiv.prodProdProdComm R M₁ M₂ N₁ N₂, map_app' := ⋯ }
Instances For
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]
[CovariantClass P P (fun (x1 x2 : P) => x1 + x2) fun (x1 x2 : P) => x1 ≤ x2]
{Q₁ : QuadraticMap R M₁ P}
{Q₂ : QuadraticMap R M₂ P}
:
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]
[CovariantClass P P (fun (x1 x2 : P) => x1 + x2) fun (x1 x2 : P) => x1 ≤ x2]
{Q₁ : QuadraticMap R M₁ P}
{Q₂ : QuadraticMap R M₂ P}
:
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]
[CovariantClass P P (fun (x1 x2 : P) => x1 + x2) fun (x1 x2 : P) => x1 ≤ x2]
{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 : 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
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₁' : 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₂' : 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 : M₁ × M₂)
(y : M₁ × M₂)
:
QuadraticMap.polar (⇑(Q₁.prod Q₂)) x y = QuadraticMap.polar (⇑Q₁) x.1 y.1 + QuadraticMap.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)
:
QuadraticMap.associated (Q₁.prod Q₂) = LinearMap.compl₁₂ (QuadraticMap.associated Q₁) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ (QuadraticMap.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.
Equations
- QuadraticMap.pi Q = ∑ i : ι, (Q i).comp (LinearMap.proj i)
Instances For
@[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)
:
(QuadraticMap.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)
:
(QuadraticMap.pi Q) (Pi.single i m) = (Q i) m
@[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))
:
(QuadraticMap.IsometryEquiv.pi e).toLinearEquiv = LinearEquiv.piCongrRight fun (i : ι) => (e i).toLinearEquiv
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.
Equations
- QuadraticMap.IsometryEquiv.pi e = { toLinearEquiv := LinearEquiv.piCongrRight fun (i : ι) => (e i).toLinearEquiv, map_app' := ⋯ }
Instances For
@[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 : ι)
:
(QuadraticMap.Isometry.single Q i) x j = Pi.single i x j
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ᵢ QuadraticMap.pi Q
LinearMap.single as an isometry.
Equations
- QuadraticMap.Isometry.single Q i = { toLinearMap := LinearMap.single R Mᵢ i, map_app' := ⋯ }
Instances For
@[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)
:
(QuadraticMap.Isometry.proj i Q) f = f i
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)
:
QuadraticMap.pi (Pi.single i Q) →qᵢ Q
LinearMap.proj as an isometry, when all but one quadratic form is zero.
Equations
- QuadraticMap.Isometry.proj i Q = { toLinearMap := LinearMap.proj i, map_app' := ⋯ }
Instances For
@[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)
:
(QuadraticMap.Isometry.proj i Q).comp (QuadraticMap.Isometry.single (Pi.single i Q) i) = QuadraticMap.Isometry.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)
:
(QuadraticMap.Isometry.proj i Q).comp (QuadraticMap.Isometry.single (Pi.single i Q) j) = QuadraticMap.Isometry.comp 0 (QuadraticMap.Isometry.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 : (QuadraticMap.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 ι]
[OrderedAddCommMonoid P]
[Module R P]
{Q : (i : ι) → QuadraticMap R (Mᵢ i) P}
:
(∀ (x : (i : ι) → Mᵢ i), 0 ≤ (QuadraticMap.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 ι]
[OrderedAddCommMonoid P]
[Module R P]
{Q : (i : ι) → QuadraticMap R (Mᵢ i) P}
:
(QuadraticMap.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 : (i : ι) → Mᵢ i)
(y : (i : ι) → Mᵢ i)
:
QuadraticMap.polar (⇑(QuadraticMap.pi Q)) x y = ∑ i : ι, QuadraticMap.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)
:
(QuadraticMap.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)
:
QuadraticMap.associated (QuadraticMap.pi Q) = ∑ i : ι, LinearMap.compl₁₂ (QuadraticMap.associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)