From 7efc2de97dcb4cfb312c20f159fb4dab89336583 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Wed, 27 Nov 2024 20:32:44 +0000 Subject: [PATCH] Progress --- Mathlib/LinearAlgebra/QuadraticForm/Basis.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basis.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basis.lean index 48dd6871b102a..aaf489a17576f 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basis.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basis.lean @@ -218,6 +218,7 @@ lemma tensorDistriFree_polar BilinMap.tensorDistrib_tmul, below_diag Q₁ bm₁ j₁ i₁ h₁, zero_tmul, add_zero, above_diag Q₁ bm₁ i₁ j₁ h₁, above_diag Q₂ bm₂ i₂ j₂ h₂] +/- lemma tensorDistriFree_polar_self (i₁ : ι₁) (i₂ : ι₂) : polar (tensorDistribFree R A bm₁ bm₂ (Q₁ ⊗ₜ Q₂)) (bm₁ i₁ ⊗ₜ bm₂ i₂) (bm₁ i₁ ⊗ₜ bm₂ i₂) = @@ -226,19 +227,25 @@ lemma tensorDistriFree_polar_self BilinMap.tensorDistrib_tmul] rw [← BilinMap.toQuadraticMap_apply, toQuadraticMap_toBilin] rw [← BilinMap.toQuadraticMap_apply, toQuadraticMap_toBilin] +-/ theorem qt_expansion (x : M₁ ⊗[R] M₂) : let Q := (tensorDistribFree R A bm₁ bm₂ (Q₁ ⊗ₜ Q₂)) - let bm : Basis (ι₁ ×ₗ ι₂) A (M₁ ⊗[R] M₂) := (bm₁.tensorProduct bm₂) - Q x = ((bm.repr x).sum fun i r => (r * r) • Q (bm i)) + + let bm : Basis (ι₁ × ι₂) A (M₁ ⊗[R] M₂) := (bm₁.tensorProduct bm₂) + Q x = ((bm.repr x).sum fun i r => (r * r) • (Q₁ (bm₁ i.1) ⊗ₜ[R] Q₂ (bm₂ i.2))) + ∑ p ∈ (bm.repr x).support.sym2 with ¬ p.IsDiag, Sym2.lift ⟨fun i j => ((bm.repr x) i) • ((bm.repr x) j) • (polar Q) (bm i) (bm j), fun i j => by simp only [polar_comm] rw [smul_comm]⟩ p := by let Q := (tensorDistribFree R A bm₁ bm₂ (Q₁ ⊗ₜ Q₂)) - let bm : Basis (ι₁ ×ₗ ι₂) A (M₁ ⊗[R] M₂) := (bm₁.tensorProduct bm₂) + let bm : Basis (ι₁ × ι₂) A (M₁ ⊗[R] M₂) := (bm₁.tensorProduct bm₂) simp_rw [basis_expansion Q bm x] + have e2 (i : ι₁ × ι₂) : bm i = bm₁ i.1 ⊗ₜ bm₂ i.2 := by + rw [← Basis.tensorProduct_apply] + have e1 (i : ι₁ × ι₂) : Q (bm i) = Q₁ (bm₁ i.1) ⊗ₜ Q₂ (bm₂ i.2) := by + rw [e2, tensorDistriFree_tmul] + simp_rw [← e1] end TensorProduct