Skip to content

Commit 8f95ac4

Browse files
Parcly-TaxelParcly-Taxel
committed
feat: port LinearAlgebra.QuadraticForm.Prod (#4735)
1 parent 892102c commit 8f95ac4

File tree

2 files changed

+198
-0
lines changed

2 files changed

+198
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1901,6 +1901,7 @@ import Mathlib.LinearAlgebra.ProjectiveSpace.Subspace
19011901
import Mathlib.LinearAlgebra.QuadraticForm.Basic
19021902
import Mathlib.LinearAlgebra.QuadraticForm.Complex
19031903
import Mathlib.LinearAlgebra.QuadraticForm.Isometry
1904+
import Mathlib.LinearAlgebra.QuadraticForm.Prod
19041905
import Mathlib.LinearAlgebra.Quotient
19051906
import Mathlib.LinearAlgebra.QuotientPi
19061907
import Mathlib.LinearAlgebra.Ray

‎Mathlib/LinearAlgebra/QuadraticForm/Prod.lean‎

Lines changed: 197 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,197 @@
1+
/-
2+
Copyright (c) 2021 Eric Wieser. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Eric Wieser
5+
6+
! This file was ported from Lean 3 source module linear_algebra.quadratic_form.prod
7+
! leanprover-community/mathlib commit 9b2755b951bc323c962bd072cd447b375cf58101
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.LinearAlgebra.QuadraticForm.Isometry
12+
13+
/-! # Quadratic form on product and pi types
14+
15+
## Main definitions
16+
17+
* `QuadraticForm.prod Q₁ Q₂`: the quadratic form constructed elementwise on a product
18+
* `QuadraticForm.pi Q`: the quadratic form constructed elementwise on a pi type
19+
20+
## Main results
21+
22+
* `QuadraticForm.Equivalent.prod`, `QuadraticForm.Equivalent.pi`: quadratic forms are equivalent
23+
if their components are equivalent
24+
* `QuadraticForm.nonneg_prod_iff`, `QuadraticForm.nonneg_pi_iff`: quadratic forms are positive-
25+
semidefinite if and only if their components are positive-semidefinite.
26+
* `QuadraticForm.posDef_prod_iff`, `QuadraticForm.posDef_pi_iff`: quadratic forms are positive-
27+
definite if and only if their components are positive-definite.
28+
29+
## Implementation notes
30+
31+
Many of the lemmas in this file could be generalized into results about sums of positive and
32+
non-negative elements, and would generalize to any map `Q` where `Q 0 = 0`, not just quadratic
33+
forms specifically.
34+
35+
-/
36+
37+
38+
universe u v w
39+
40+
variable {ι : Type _} {R : Type _} {M₁ M₂ N₁ N₂ : Type _} {Mᵢ Nᵢ : ι → Type _}
41+
42+
variable [Semiring R]
43+
44+
variable [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂]
45+
46+
variable [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂]
47+
48+
variable [∀ i, AddCommMonoid (Mᵢ i)] [∀ i, AddCommMonoid (Nᵢ i)]
49+
50+
variable [∀ i, Module R (Mᵢ i)] [∀ i, Module R (Nᵢ i)]
51+
52+
namespace QuadraticForm
53+
54+
/-- Construct a quadratic form on a product of two modules from the quadratic form on each module.
55+
-/
56+
@[simps!]
57+
def prod (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm R (M₁ × M₂) :=
58+
Q₁.comp (LinearMap.fst _ _ _) + Q₂.comp (LinearMap.snd _ _ _)
59+
#align quadratic_form.prod QuadraticForm.prod
60+
61+
/-- An isometry between quadratic forms generated by `QuadraticForm.prod` can be constructed
62+
from a pair of isometries between the left and right parts. -/
63+
@[simps toLinearEquiv]
64+
def Isometry.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₁' : QuadraticForm R N₁}
65+
{Q₂' : QuadraticForm R N₂} (e₁ : Q₁.Isometry Q₁') (e₂ : Q₂.Isometry Q₂') :
66+
(Q₁.prod Q₂).Isometry (Q₁'.prod Q₂') where
67+
map_app' x := congr_arg₂ (· + ·) (e₁.map_app x.1) (e₂.map_app x.2)
68+
toLinearEquiv := LinearEquiv.prod e₁.toLinearEquiv e₂.toLinearEquiv
69+
#align quadratic_form.isometry.prod QuadraticForm.Isometry.prod
70+
71+
theorem Equivalent.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
72+
{Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} (e₁ : Q₁.Equivalent Q₁')
73+
(e₂ : Q₂.Equivalent Q₂') : (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂') :=
74+
Nonempty.map2 Isometry.prod e₁ e₂
75+
#align quadratic_form.equivalent.prod QuadraticForm.Equivalent.prod
76+
77+
/-- If a product is anisotropic then its components must be. The converse is not true. -/
78+
theorem anisotropic_of_prod {R} [OrderedRing R] [Module R M₁] [Module R M₂]
79+
{Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : (Q₁.prod Q₂).Anisotropic) :
80+
Q₁.Anisotropic ∧ Q₂.Anisotropic := by
81+
simp_rw [Anisotropic, prod_apply, Prod.forall, Prod.mk_eq_zero] at h
82+
constructor
83+
· intro x hx
84+
refine' (h x 0 _).1
85+
rw [hx, zero_add, map_zero]
86+
· intro x hx
87+
refine' (h 0 x _).2
88+
rw [hx, add_zero, map_zero]
89+
#align quadratic_form.anisotropic_of_prod QuadraticForm.anisotropic_of_prod
90+
91+
theorem nonneg_prod_iff {R} [OrderedRing R] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁}
92+
{Q₂ : QuadraticForm R M₂} : (∀ x, 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ x, 0 ≤ Q₁ x) ∧ ∀ x, 0 ≤ Q₂ x := by
93+
simp_rw [Prod.forall, prod_apply]
94+
constructor
95+
· intro h
96+
constructor
97+
· intro x; simpa only [add_zero, map_zero] using h x 0
98+
· intro x; simpa only [zero_add, map_zero] using h 0 x
99+
· rintro ⟨h₁, h₂⟩ x₁ x₂
100+
exact add_nonneg (h₁ x₁) (h₂ x₂)
101+
#align quadratic_form.nonneg_prod_iff QuadraticForm.nonneg_prod_iff
102+
103+
theorem posDef_prod_iff {R} [OrderedRing R] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁}
104+
{Q₂ : QuadraticForm R M₂} : (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef := by
105+
simp_rw [posDef_iff_nonneg, nonneg_prod_iff]
106+
constructor
107+
· rintro ⟨⟨hle₁, hle₂⟩, ha⟩
108+
obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
109+
refine' ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
110+
· rintro ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
111+
refine' ⟨⟨hle₁, hle₂⟩, _⟩
112+
rintro ⟨x₁, x₂⟩ (hx : Q₁ x₁ + Q₂ x₂ = 0)
113+
rw [add_eq_zero_iff' (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
114+
rwa [Prod.mk_eq_zero]
115+
#align quadratic_form.pos_def_prod_iff QuadraticForm.posDef_prod_iff
116+
117+
theorem PosDef.prod {R} [OrderedRing R] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁}
118+
{Q₂ : QuadraticForm R M₂} (h₁ : Q₁.PosDef) (h₂ : Q₂.PosDef) : (Q₁.prod Q₂).PosDef :=
119+
posDef_prod_iff.mpr ⟨h₁, h₂⟩
120+
#align quadratic_form.pos_def.prod QuadraticForm.PosDef.prod
121+
122+
open scoped BigOperators
123+
124+
/-- Construct a quadratic form on a family of modules from the quadratic form on each module. -/
125+
def pi [Fintype ι] (Q : ∀ i, QuadraticForm R (Mᵢ i)) : QuadraticForm R (∀ i, Mᵢ i) :=
126+
∑ i, (Q i).comp (LinearMap.proj i : _ →ₗ[R] Mᵢ i)
127+
#align quadratic_form.pi QuadraticForm.pi
128+
129+
@[simp]
130+
theorem pi_apply [Fintype ι] (Q : ∀ i, QuadraticForm R (Mᵢ i)) (x : ∀ i, Mᵢ i) :
131+
pi Q x = ∑ i, Q i (x i) :=
132+
sum_apply _ _ _
133+
#align quadratic_form.pi_apply QuadraticForm.pi_apply
134+
135+
/-- An isometry between quadratic forms generated by `QuadraticForm.pi` can be constructed
136+
from a pair of isometries between the left and right parts. -/
137+
@[simps toLinearEquiv]
138+
def Isometry.pi [Fintype ι] {Q : ∀ i, QuadraticForm R (Mᵢ i)} {Q' : ∀ i, QuadraticForm R (Nᵢ i)}
139+
(e : ∀ i, (Q i).Isometry (Q' i)) : (pi Q).Isometry (pi Q') where
140+
map_app' x := by
141+
simp only [pi_apply, LinearEquiv.piCongrRight, LinearEquiv.toFun_eq_coe,
142+
Isometry.coe_toLinearEquiv, Isometry.map_app]
143+
toLinearEquiv := LinearEquiv.piCongrRight fun i => (e i : Mᵢ i ≃ₗ[R] Nᵢ i)
144+
#align quadratic_form.isometry.pi QuadraticForm.Isometry.pi
145+
146+
theorem Equivalent.pi [Fintype ι] {Q : ∀ i, QuadraticForm R (Mᵢ i)}
147+
{Q' : ∀ i, QuadraticForm R (Nᵢ i)} (e : ∀ i, (Q i).Equivalent (Q' i)) :
148+
(pi Q).Equivalent (pi Q') :=
149+
⟨Isometry.pi fun i => Classical.choice (e i)⟩
150+
#align quadratic_form.equivalent.pi QuadraticForm.Equivalent.pi
151+
152+
/-- If a family is anisotropic then its components must be. The converse is not true. -/
153+
theorem anisotropic_of_pi [Fintype ι] {R} [OrderedRing R] [∀ i, Module R (Mᵢ i)]
154+
{Q : ∀ i, QuadraticForm R (Mᵢ i)} (h : (pi Q).Anisotropic) : ∀ i, (Q i).Anisotropic := by
155+
simp_rw [Anisotropic, pi_apply, Function.funext_iff, Pi.zero_apply] at h
156+
intro i x hx
157+
classical
158+
have := h (Pi.single i x) ?_ i
159+
· rw [Pi.single_eq_same] at this
160+
exact this
161+
apply Finset.sum_eq_zero
162+
intro j _
163+
by_cases hji : j = i
164+
· subst hji; rw [Pi.single_eq_same, hx]
165+
· rw [Pi.single_eq_of_ne hji, map_zero]
166+
#align quadratic_form.anisotropic_of_pi QuadraticForm.anisotropic_of_pi
167+
168+
theorem nonneg_pi_iff [Fintype ι] {R} [OrderedRing R] [∀ i, Module R (Mᵢ i)]
169+
{Q : ∀ i, QuadraticForm R (Mᵢ i)} : (∀ x, 0 ≤ pi Q x) ↔ ∀ i x, 0 ≤ Q i x := by
170+
simp_rw [pi, sum_apply, comp_apply, LinearMap.proj_apply]
171+
dsimp only
172+
constructor
173+
-- TODO: does this generalize to a useful lemma independent of `QuadraticForm`?
174+
· intro h i x
175+
classical
176+
convert h (Pi.single i x) using 1
177+
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hji => ?_, Pi.single_eq_same]
178+
rw [Pi.single_eq_of_ne hji, map_zero]
179+
· rintro h x
180+
exact Finset.sum_nonneg fun i _ => h i (x i)
181+
#align quadratic_form.nonneg_pi_iff QuadraticForm.nonneg_pi_iff
182+
183+
theorem posDef_pi_iff [Fintype ι] {R} [OrderedRing R] [∀ i, Module R (Mᵢ i)]
184+
{Q : ∀ i, QuadraticForm R (Mᵢ i)} : (pi Q).PosDef ↔ ∀ i, (Q i).PosDef := by
185+
simp_rw [posDef_iff_nonneg, nonneg_pi_iff]
186+
constructor
187+
· rintro ⟨hle, ha⟩
188+
intro i
189+
exact ⟨hle i, anisotropic_of_pi ha i⟩
190+
· intro h
191+
refine' ⟨fun i => (h i).1, fun x hx => funext fun i => (h i).2 _ _⟩
192+
rw [pi_apply, Finset.sum_eq_zero_iff_of_nonneg fun j _ => ?_] at hx
193+
· exact hx _ (Finset.mem_univ _)
194+
exact (h j).1 _
195+
#align quadratic_form.pos_def_pi_iff QuadraticForm.posDef_pi_iff
196+
197+
end QuadraticForm

0 commit comments

Comments
 (0)