From 250f93731867004e2e0cc8531ad20f194f4257fc Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sun, 21 Jul 2024 16:30:02 +0100 Subject: [PATCH 01/49] Make LinearMap.BilinMap.tensorDistrib work for bilinear maps --- .../BilinearForm/TensorProduct.lean | 33 +++++++++++-------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index bea71533f32d4..398e5968b5d16 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -20,9 +20,10 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower suppress_compilation -universe u v w uι uR uA uM₁ uM₂ +universe u v w uι uR uA uM₁ uM₂ uN₁ uN₂ -variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} +variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} + {N₂ : Type uN₂} open TensorProduct @@ -35,24 +36,28 @@ open LinearMap (BilinForm) section CommSemiring variable [CommSemiring R] [CommSemiring A] -variable [AddCommMonoid M₁] [AddCommMonoid M₂] -variable [Algebra R A] [Module R M₁] [Module A M₁] +variable [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] +variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] -variable [Module R M₂] +variable [SMulCommClass R A N₁] [SMulCommClass A R N₁] [IsScalarTower R A N₁] +variable [Module R M₂] [Module R N₂] variable (R A) in -/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. - -Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra -over the ring in which the right bilinear form is valued. -/ -def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap - ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm).toLinearMap - ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _ +/-- The tensor product of two bilinear maps injects into bilinear maps on tensor products. + +Note this is heterobasic; the bilinear map on the left can take values in a module over a +(commutative) algebra over the ring of the module in which the right bilinear map is valued. -/ +def tensorDistrib : + BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂ →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := + (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ + ((LinearMap.llcomp A _ _ _).flip + (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap) + ∘ₗ TensorProduct.AlgebraTensorModule.homTensorHomMap R _ _ _ _ _ _ ∘ₗ (TensorProduct.AlgebraTensorModule.congr - (TensorProduct.lift.equiv A M₁ M₁ A) + (TensorProduct.lift.equiv A M₁ M₁ N₁) (TensorProduct.lift.equiv R _ _ _)).toLinearMap + -- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for -- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306. @[simp] From 84767099d3f5a73fd9dc53016dc655d13c6c953c Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sun, 21 Jul 2024 20:59:44 +0100 Subject: [PATCH 02/49] Progress --- .../BilinearForm/TensorProduct.lean | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 398e5968b5d16..07c24657cdc75 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -48,7 +48,7 @@ variable (R A) in Note this is heterobasic; the bilinear map on the left can take values in a module over a (commutative) algebra over the ring of the module in which the right bilinear map is valued. -/ def tensorDistrib : - BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂ →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := + (BilinMap A M₁ N₁) ⊗[R] (BilinMap R M₂ N₂) →ₗ[A] (BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) := (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ ((LinearMap.llcomp A _ _ _).flip (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap) @@ -58,17 +58,16 @@ def tensorDistrib : (TensorProduct.lift.equiv R _ _ _)).toLinearMap --- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for --- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306. @[simp] -theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = B₂ m₂ m₂' • B₁ m₁ m₁' := + = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' := rfl /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -protected abbrev tmul (B₁ : BilinMap A M₁ A) (B₂ : BilinMap R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A := +protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : + BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := tensorDistrib R A (B₁ ⊗ₜ[R] B₂) attribute [local ext] TensorProduct.ext in @@ -81,13 +80,13 @@ lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R variable (A) in /-- The base change of a bilinear form. -/ -protected def baseChange (B : BilinMap R M₂ R) : BilinForm A (A ⊗[R] M₂) := +protected def baseChange (B : BilinMap R M₂ N₂) : BilinMap A (A ⊗[R] M₂) (A ⊗[R] N₂) := BilinMap.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B @[simp] theorem baseChange_tmul (B₂ : BilinMap R M₂ R) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : - B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := + B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') ⊗ₜ (B₂ m₂ m₂') := rfl variable (A) in @@ -109,7 +108,7 @@ variable [Nontrivial R] variable (R) in /-- `tensorDistrib` as an equivalence. -/ noncomputable def tensorDistribEquiv : - BilinForm R M₁ ⊗[R] BilinForm R M₂ ≃ₗ[R] BilinForm R (M₁ ⊗[R] M₂) := + BilinMap R M₁ R ⊗[R] BilinMap R M₂ R ≃ₗ[R] BilinMap R (M₁ ⊗[R] M₂) (R ⊗[R] R) := -- the same `LinearEquiv`s as from `tensorDistrib`, -- but with the inner linear map also as an equiv TensorProduct.congr (TensorProduct.lift.equiv R _ _ _) (TensorProduct.lift.equiv R _ _ _) ≪≫ₗ @@ -118,7 +117,7 @@ noncomputable def tensorDistribEquiv : (TensorProduct.lift.equiv R _ _ _).symm @[simp] -theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistribEquiv_tmul (B₁ : BilinMap R M₁ R) (B₂ : BilinMap R M₂ R) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := From 7f4b8b43c96d2f8762435e650f86250726aecb98 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sun, 21 Jul 2024 21:18:13 +0100 Subject: [PATCH 03/49] Get LinearAlgebra/BilinearForm/TensorProduct to build by commenting stuff out --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 07c24657cdc75..6f5e0161f431b 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -70,6 +70,7 @@ protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := tensorDistrib R A (B₁ ⊗ₜ[R] B₂) +/- attribute [local ext] TensorProduct.ext in /-- A tensor product of symmetric bilinear forms is symmetric. -/ lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R M₂ R} @@ -77,6 +78,7 @@ lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R rw [LinearMap.isSymm_iff_eq_flip] ext x₁ x₂ y₁ y₂ exact congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁) +-/ variable (A) in /-- The base change of a bilinear form. -/ @@ -89,10 +91,12 @@ theorem baseChange_tmul (B₂ : BilinMap R M₂ R) (a : A) (m₂ : M₂) B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') ⊗ₜ (B₂ m₂ m₂') := rfl +/- variable (A) in /-- The base change of a symmetric bilinear form is symmetric. -/ lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm := IsSymm.tmul mul_comm hB₂ +-/ end CommSemiring @@ -105,6 +109,7 @@ variable [Module.Free R M₁] [Module.Finite R M₁] variable [Module.Free R M₂] [Module.Finite R M₂] variable [Nontrivial R] +/- variable (R) in /-- `tensorDistrib` as an equivalence. -/ noncomputable def tensorDistribEquiv : @@ -116,6 +121,7 @@ noncomputable def tensorDistribEquiv : (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ (TensorProduct.lift.equiv R _ _ _).symm + @[simp] theorem tensorDistribEquiv_tmul (B₁ : BilinMap R M₁ R) (B₂ : BilinMap R M₂ R) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : @@ -136,6 +142,7 @@ theorem tensorDistribEquiv_toLinearMap : theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B := DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B +-/ end CommRing From 3dcc169d629cb0485f17191aa85329e48de95991 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sun, 21 Jul 2024 21:18:54 +0100 Subject: [PATCH 04/49] Get LinearAlgebra/QuadraticForm/TensorProduct to build by commenting stuff out --- .../QuadraticForm/TensorProduct.lean | 39 +++++++++++-------- 1 file changed, 22 insertions(+), 17 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 54a0bb985a977..f69033a23b4af 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -16,23 +16,24 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic -/ -universe uR uA uM₁ uM₂ +universe uR uA uM₁ uM₂ uN₁ uN₂ -variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} +variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uM₁} {N₂ : Type uM₂} open TensorProduct open LinearMap (BilinMap) open LinearMap (BilinForm) open QuadraticMap -namespace QuadraticForm +namespace QuadraticMap section CommRing variable [CommRing R] [CommRing A] -variable [AddCommGroup M₁] [AddCommGroup M₂] -variable [Algebra R A] [Module R M₁] [Module A M₁] +variable [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] +variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] -variable [Module R M₂] [Invertible (2 : R)] +variable [SMulCommClass R A N₁] [SMulCommClass A R N₁] [IsScalarTower R A N₁] +variable [Module R M₂] [Module R N₂] [Invertible (2 : R)] variable (R A) in @@ -42,36 +43,38 @@ Note this is heterobasic; the quadratic form on the left can take values in a la the one on the right. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 noncomputable def tensorDistrib : - QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := + QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm -- while `letI`s would produce a better term than `let`, they would make this already-slow -- definition even slower. let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map - (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) + (QuadraticMap.associated : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁) + (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) toQ ∘ₗ tmulB ∘ₗ toB -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for -- `R = A` of `Q₁ m₁ * Q₂ m₂`. @[simp] -theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) : - tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ := +theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) + (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 -protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : - QuadraticForm A (M₁ ⊗[R] M₂) := +protected noncomputable abbrev tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) : + QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) -theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : - associated (R := A) (Q₁.tmul Q₂) +/- + +theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) + (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by - rw [QuadraticForm.tmul, tensorDistrib, BilinMap.tmul] + rw [QuadraticMap.tmul, tensorDistrib, BilinMap.tmul] dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) @@ -106,6 +109,8 @@ theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq, smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul] +-/ + /-- If two quadratic forms from `A ⊗[R] M₂` agree on elements of the form `1 ⊗ m`, they are equal. In other words, if a base change exists for a quadratic form, it is unique. @@ -132,4 +137,4 @@ theorem baseChange_ext ⦃Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)⦄ end CommRing -end QuadraticForm +end QuadraticMap From 8eb13e54f292887f04c386ba6f6267021a9bd811 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sun, 21 Jul 2024 22:08:51 +0100 Subject: [PATCH 05/49] Fix --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index f69033a23b4af..5c18f0d9b5a09 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -18,7 +18,7 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic universe uR uA uM₁ uM₂ uN₁ uN₂ -variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uM₁} {N₂ : Type uM₂} +variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} open TensorProduct open LinearMap (BilinMap) From 069ebbd2da930cc94c4f4c2499006e41c1627ef8 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sun, 21 Jul 2024 22:13:43 +0100 Subject: [PATCH 06/49] Add more N --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 7881341dc9216..16aef04a92418 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -874,12 +874,12 @@ theorem toQuadraticMap_associated : (associatedHom S Q).toQuadraticMap = Q := -- note: usually `rightInverse` lemmas are named the other way around, but this is consistent -- with historical naming in this file. theorem associated_rightInverse : - Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M R) := + Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M N) := fun Q => toQuadraticMap_associated S Q /-- `associated'` is the `ℤ`-linear map that sends a quadratic form on a module `M` over `R` to its associated symmetric bilinear form. -/ -abbrev associated' : QuadraticMap R M R →ₗ[ℤ] BilinMap R M R := +abbrev associated' : QuadraticMap R M N →ₗ[ℤ] BilinMap R M N := associatedHom ℤ /-- Symmetric bilinear forms can be lifted to quadratic forms -/ @@ -889,9 +889,9 @@ instance canLift : /-- There exists a non-null vector with respect to any quadratic form `Q` whose associated bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`. -/ -theorem exists_quadraticForm_ne_zero {Q : QuadraticForm R M} +theorem exists_quadraticForm_ne_zero {Q : QuadraticMap R M N} -- Porting note: added implicit argument - (hB₁ : associated' (R := R) Q ≠ 0) : + (hB₁ : associated' (R := R) (N := N) Q ≠ 0) : ∃ x, Q x ≠ 0 := by rw [← not_forall] intro h @@ -1024,7 +1024,7 @@ variable [CommRing R] [AddCommGroup M] [Module R M] theorem separatingLeft_of_anisotropic [Invertible (2 : R)] (Q : QuadraticMap R M R) (hB : Q.Anisotropic) : -- Porting note: added implicit argument - (QuadraticMap.associated' (R := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by + (QuadraticMap.associated' (R := R) (N := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by rw [← hx x] exact (associated_eq_self_apply _ _ x).symm From 4074a7987933b27375ec6f77772c797b19bef155 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 22 Jul 2024 07:52:39 +0100 Subject: [PATCH 07/49] Recover BilinForm --- .../BilinearForm/TensorProduct.lean | 41 ++++++++++++++++--- 1 file changed, 35 insertions(+), 6 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 6f5e0161f431b..63d6208e5557c 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -48,7 +48,7 @@ variable (R A) in Note this is heterobasic; the bilinear map on the left can take values in a module over a (commutative) algebra over the ring of the module in which the right bilinear map is valued. -/ def tensorDistrib : - (BilinMap A M₁ N₁) ⊗[R] (BilinMap R M₂ N₂) →ₗ[A] (BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) := + ((BilinMap A M₁ N₁) ⊗[R] (BilinMap R M₂ N₂)) →ₗ[A] ((BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))) := (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ ((LinearMap.llcomp A _ _ _).flip (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap) @@ -57,6 +57,32 @@ def tensorDistrib : (TensorProduct.lift.equiv A M₁ M₁ N₁) (TensorProduct.lift.equiv R _ _ _)).toLinearMap +/- Want to recover +BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) +-/ + +/-- This probably belongs somewhere else -/ +def congrtmp (e : N₁ ≃ₗ[R] N₂) : BilinMap R M₁ N₁ ≃ₗ[R] BilinMap R M₁ N₂ where + toFun B := LinearMap.compr₂ B e + invFun B := LinearMap.compr₂ B e.symm + left_inv B := ext₂ fun x => by + simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, implies_true] + right_inv B := ext₂ fun x => by + simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, implies_true] + map_add' B B' := ext₂ fun x y => by + simp only [compr₂_apply, add_apply, map_add, LinearEquiv.coe_coe] + map_smul' B B' := ext₂ fun x y => by + simp only [compr₂_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe, + RingHom.id_apply] + +def conjecture1 : A ⊗[R] R ≃ₗ[A] A := AlgebraTensorModule.rid R A A + +def conjecture2 : BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) ≃ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := + congrtmp conjecture1 + +variable (R A) in +def tensorDistrib' : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := + conjecture2.toLinearMap ∘ₗ (tensorDistrib R A) @[simp] theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) @@ -65,20 +91,23 @@ theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' := rfl -/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +/-- The tensor product of two bilinear maps, a shorthand for dot notation. -/ protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := tensorDistrib R A (B₁ ⊗ₜ[R] B₂) -/- +/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +protected abbrev tmul' (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : + BilinForm A (M₁ ⊗[R] M₂) := + tensorDistrib' R A (B₁ ⊗ₜ[R] B₂) + attribute [local ext] TensorProduct.ext in /-- A tensor product of symmetric bilinear forms is symmetric. -/ -lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R M₂ R} - (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by +lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} + (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul' B₂).IsSymm := by rw [LinearMap.isSymm_iff_eq_flip] ext x₁ x₂ y₁ y₂ exact congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁) --/ variable (A) in /-- The base change of a bilinear form. -/ From 2d302a63b8c15822c546754577092ada525261f3 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 22 Jul 2024 07:55:05 +0100 Subject: [PATCH 08/49] Tidy uo --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 63d6208e5557c..8d33e53b5b8da 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -75,14 +75,9 @@ def congrtmp (e : N₁ ≃ₗ[R] N₂) : BilinMap R M₁ N₁ ≃ₗ[R] BilinMap simp only [compr₂_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe, RingHom.id_apply] -def conjecture1 : A ⊗[R] R ≃ₗ[A] A := AlgebraTensorModule.rid R A A - -def conjecture2 : BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) ≃ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - congrtmp conjecture1 - variable (R A) in def tensorDistrib' : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - conjecture2.toLinearMap ∘ₗ (tensorDistrib R A) + (congrtmp (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib R A) @[simp] theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) From 0491c558db658fcaa3ee4f2ae36e22fa5a51b65d Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 22 Jul 2024 20:47:33 +0100 Subject: [PATCH 09/49] Just try to get it building --- .../BilinearForm/TensorProduct.lean | 53 +++++++++---------- .../QuadraticForm/TensorProduct.lean | 4 +- 2 files changed, 28 insertions(+), 29 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 8d33e53b5b8da..cd139c52caf22 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -47,7 +47,7 @@ variable (R A) in Note this is heterobasic; the bilinear map on the left can take values in a module over a (commutative) algebra over the ring of the module in which the right bilinear map is valued. -/ -def tensorDistrib : +def tensorDistrib' : ((BilinMap A M₁ N₁) ⊗[R] (BilinMap R M₂ N₂)) →ₗ[A] ((BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))) := (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ ((LinearMap.llcomp A _ _ _).flip @@ -57,9 +57,11 @@ def tensorDistrib : (TensorProduct.lift.equiv A M₁ M₁ N₁) (TensorProduct.lift.equiv R _ _ _)).toLinearMap -/- Want to recover -BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) --/ +theorem tensorDistrib_tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) + (m₁' : M₁) (m₂' : M₂) : + tensorDistrib' R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' := + rfl /-- This probably belongs somewhere else -/ def congrtmp (e : N₁ ≃ₗ[R] N₂) : BilinMap R M₁ N₁ ≃ₗ[R] BilinMap R M₁ N₂ where @@ -76,51 +78,51 @@ def congrtmp (e : N₁ ≃ₗ[R] N₂) : BilinMap R M₁ N₁ ≃ₗ[R] BilinMap RingHom.id_apply] variable (R A) in -def tensorDistrib' : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - (congrtmp (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib R A) +/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. +Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra +over the ring in which the right bilinear form is valued. -/ +def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := + (congrtmp (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) + +variable (R A) in + +-- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for +-- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306. @[simp] -theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' := + = B₂ m₂ m₂' • B₁ m₁ m₁' := rfl -/-- The tensor product of two bilinear maps, a shorthand for dot notation. -/ -protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : - BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := - tensorDistrib R A (B₁ ⊗ₜ[R] B₂) - /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -protected abbrev tmul' (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : - BilinForm A (M₁ ⊗[R] M₂) := - tensorDistrib' R A (B₁ ⊗ₜ[R] B₂) +protected abbrev tmul (B₁ : BilinMap A M₁ A) (B₂ : BilinMap R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A := + tensorDistrib R A (B₁ ⊗ₜ[R] B₂) attribute [local ext] TensorProduct.ext in /-- A tensor product of symmetric bilinear forms is symmetric. -/ -lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} - (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul' B₂).IsSymm := by +lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R M₂ R} + (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by rw [LinearMap.isSymm_iff_eq_flip] ext x₁ x₂ y₁ y₂ exact congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁) variable (A) in /-- The base change of a bilinear form. -/ -protected def baseChange (B : BilinMap R M₂ N₂) : BilinMap A (A ⊗[R] M₂) (A ⊗[R] N₂) := +protected def baseChange (B : BilinMap R M₂ R) : BilinForm A (A ⊗[R] M₂) := BilinMap.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B @[simp] theorem baseChange_tmul (B₂ : BilinMap R M₂ R) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : - B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') ⊗ₜ (B₂ m₂ m₂') := + B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := rfl -/- variable (A) in /-- The base change of a symmetric bilinear form is symmetric. -/ lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm := IsSymm.tmul mul_comm hB₂ --/ end CommSemiring @@ -133,11 +135,10 @@ variable [Module.Free R M₁] [Module.Finite R M₁] variable [Module.Free R M₂] [Module.Finite R M₂] variable [Nontrivial R] -/- variable (R) in /-- `tensorDistrib` as an equivalence. -/ noncomputable def tensorDistribEquiv : - BilinMap R M₁ R ⊗[R] BilinMap R M₂ R ≃ₗ[R] BilinMap R (M₁ ⊗[R] M₂) (R ⊗[R] R) := + BilinForm R M₁ ⊗[R] BilinForm R M₂ ≃ₗ[R] BilinForm R (M₁ ⊗[R] M₂) := -- the same `LinearEquiv`s as from `tensorDistrib`, -- but with the inner linear map also as an equiv TensorProduct.congr (TensorProduct.lift.equiv R _ _ _) (TensorProduct.lift.equiv R _ _ _) ≪≫ₗ @@ -145,9 +146,8 @@ noncomputable def tensorDistribEquiv : (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ (TensorProduct.lift.equiv R _ _ _).symm - @[simp] -theorem tensorDistribEquiv_tmul (B₁ : BilinMap R M₁ R) (B₂ : BilinMap R M₂ R) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := @@ -166,7 +166,6 @@ theorem tensorDistribEquiv_toLinearMap : theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B := DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B --/ end CommRing diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 5c18f0d9b5a09..bcb6d7037a67a 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -48,7 +48,7 @@ noncomputable def tensorDistrib : -- while `letI`s would produce a better term than `let`, they would make this already-slow -- definition even slower. let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) - let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + let tmulB := BilinMap.tensorDistrib' R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map (QuadraticMap.associated : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁) (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) @@ -60,7 +60,7 @@ noncomputable def tensorDistrib : theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _ + (BilinMap.tensorDistrib_tmul' _ _ _ _ _ _).trans <| congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ From 12e8ccb66779f3e6d22f95e390b0fef63ee32fcd Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 22 Jul 2024 21:53:25 +0100 Subject: [PATCH 10/49] Mostly put it back together --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 20 +++++ .../BilinearForm/TensorProduct.lean | 18 +---- .../QuadraticForm/TensorProduct.lean | 77 ++++++++++++++----- 3 files changed, 82 insertions(+), 33 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index 1b4cb8e10bb56..ed951ddec61db 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -39,6 +39,7 @@ Bilinear form, -/ open LinearMap (BilinForm) +open LinearMap (BilinMap) universe u v w @@ -305,6 +306,25 @@ theorem comp_congr (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l r : M' →ₗ[R B.comp (l.comp (e.symm : M'' →ₗ[R] M')) (r.comp (e.symm : M'' →ₗ[R] M')) := rfl +variable {N₁ N₂ : Type*} +variable [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] + +/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear +maps into `N₂`. -/ +@[simps] +def _root_.LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ where + toFun B := LinearMap.compr₂ B e + invFun B := LinearMap.compr₂ B e.symm + left_inv B := ext₂ fun x => by + simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, implies_true] + right_inv B := ext₂ fun x => by + simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, implies_true] + map_add' B B' := ext₂ fun x y => by + simp only [compr₂_apply, LinearMap.add_apply, map_add, LinearEquiv.coe_coe] + map_smul' B B' := ext₂ fun x y => by + simp only [compr₂_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe, + RingHom.id_apply] + end congr section LinMulLin diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index cd139c52caf22..f0cf6f234f9f3 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -5,6 +5,7 @@ Authors: Eric Wieser -/ import Mathlib.LinearAlgebra.Dual import Mathlib.LinearAlgebra.TensorProduct.Tower +import Mathlib.LinearAlgebra.BilinearForm.Hom /-! # The bilinear form on a tensor product @@ -57,33 +58,20 @@ def tensorDistrib' : (TensorProduct.lift.equiv A M₁ M₁ N₁) (TensorProduct.lift.equiv R _ _ _)).toLinearMap +@[simp] theorem tensorDistrib_tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistrib' R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' := rfl -/-- This probably belongs somewhere else -/ -def congrtmp (e : N₁ ≃ₗ[R] N₂) : BilinMap R M₁ N₁ ≃ₗ[R] BilinMap R M₁ N₂ where - toFun B := LinearMap.compr₂ B e - invFun B := LinearMap.compr₂ B e.symm - left_inv B := ext₂ fun x => by - simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, implies_true] - right_inv B := ext₂ fun x => by - simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, implies_true] - map_add' B B' := ext₂ fun x y => by - simp only [compr₂_apply, add_apply, map_add, LinearEquiv.coe_coe] - map_smul' B B' := ext₂ fun x y => by - simp only [compr₂_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe, - RingHom.id_apply] - variable (R A) in /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra over the ring in which the right bilinear form is valued. -/ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - (congrtmp (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) + (congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) variable (R A) in diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index bcb6d7037a67a..a46b4e17280eb 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -25,7 +25,7 @@ open LinearMap (BilinMap) open LinearMap (BilinForm) open QuadraticMap -namespace QuadraticMap +namespace QuadraticForm section CommRing variable [CommRing R] [CommRing A] @@ -35,14 +35,30 @@ variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M variable [SMulCommClass R A N₁] [SMulCommClass A R N₁] [IsScalarTower R A N₁] variable [Module R M₂] [Module R N₂] [Invertible (2 : R)] +/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear +maps into `N₂`. -/ +@[simps] +def congr₂ (e : N₁ ≃ₗ[R] N₂) : QuadraticMap R M₁ N₁ ≃ₗ[R] QuadraticMap R M₁ N₂ where + toFun Q := e.compQuadraticMap Q + invFun Q := e.symm.compQuadraticMap Q + left_inv _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] + right_inv _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] + map_add' _ _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, add_apply, map_add, LinearEquiv.coe_coe] + map_smul' _ _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, smul_apply, LinearMapClass.map_smul, + LinearEquiv.coe_coe, RingHom.id_apply] + variable (R A) in -/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. +/-- The tensor product of two quadratic maps injects into quadratic maps on tensor products. -Note this is heterobasic; the quadratic form on the left can take values in a larger ring than -the one on the right. -/ +Note this is heterobasic; the quadratic map on the left can take values in a module over a larger +ring than the one on the right. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 -noncomputable def tensorDistrib : +noncomputable def tensorDistrib' : QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm -- while `letI`s would produce a better term than `let`, they would make this already-slow @@ -54,30 +70,57 @@ noncomputable def tensorDistrib : (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) toQ ∘ₗ tmulB ∘ₗ toB +@[simp] +theorem tensorDistrib_tmul' (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) + (m₂ : M₂) : tensorDistrib' R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + (BilinMap.tensorDistrib_tmul' _ _ _ _ _ _).trans <| congr_arg₂ _ + (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) + +/-- The tensor product of two quadratic maps, a shorthand for dot notation. -/ +-- `noncomputable` is a performance workaround for mathlib4#7103 +protected noncomputable abbrev tmul' (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) : + QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := + tensorDistrib' R A (Q₁ ⊗ₜ[R] Q₂) + +variable (R A) in +/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. + +Note this is heterobasic; the quadratic form on the left can take values in a larger ring than +the one on the right. -/ +-- `noncomputable` is a performance workaround for mathlib4#7103 +noncomputable def tensorDistrib : + QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := + (congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) + -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for -- `R = A` of `Q₁ m₁ * Q₂ m₂`. @[simp] -theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) - (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := +theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) : + tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - (BilinMap.tensorDistrib_tmul' _ _ _ _ _ _).trans <| congr_arg₂ _ + (BilinMap.tensorDistrib_tmul _ _ _ _ _ _ _ _).trans <| congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 -protected noncomputable abbrev tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) : - QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := +protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : + QuadraticForm A (M₁ ⊗[R] M₂) := tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) -/- - theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) - = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by - rw [QuadraticMap.tmul, tensorDistrib, BilinMap.tmul] - dsimp + = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by sorry +/- + rw [QuadraticMap.tmul, tensorDistrib, tensorDistrib', BilinMap.tmul, congr₂, + AlgebraTensorModule.rid] + simp_rw [LinearMap.compQuadraticMap] + --simp? + dsimp? have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) + dsimp only +-/ theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • (polarBilin Q₁).tmul (polarBilin Q₂) := by @@ -109,8 +152,6 @@ theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq, smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul] --/ - /-- If two quadratic forms from `A ⊗[R] M₂` agree on elements of the form `1 ⊗ m`, they are equal. In other words, if a base change exists for a quadratic form, it is unique. @@ -137,4 +178,4 @@ theorem baseChange_ext ⦃Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)⦄ end CommRing -end QuadraticMap +end QuadraticForm From 7530ddcccdc49ecbd34e2294622689587389818a Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 22 Jul 2024 21:59:01 +0100 Subject: [PATCH 11/49] Reorg --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 17 +++++++++++++++++ .../QuadraticForm/TensorProduct.lean | 17 ----------------- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 16aef04a92418..551e44f10d6e2 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -585,6 +585,23 @@ def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S (f : N →ₗ[S] P) (Q : QuadraticMap R M N) : QuadraticMap S M P := _root_.LinearMap.compQuadraticMap f Q.restrictScalars + +/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear +maps into `N₂`. -/ +@[simps] +def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where + toFun Q := e.compQuadraticMap Q + invFun Q := e.symm.compQuadraticMap Q + left_inv _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] + right_inv _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] + map_add' _ _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, add_apply, map_add, LinearEquiv.coe_coe] + map_smul' _ _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, smul_apply, LinearMapClass.map_smul, + LinearEquiv.coe_coe, RingHom.id_apply] + end Comp section NonUnitalNonAssocSemiring diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index a46b4e17280eb..684085230778a 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -35,23 +35,6 @@ variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M variable [SMulCommClass R A N₁] [SMulCommClass A R N₁] [IsScalarTower R A N₁] variable [Module R M₂] [Module R N₂] [Invertible (2 : R)] -/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear -maps into `N₂`. -/ -@[simps] -def congr₂ (e : N₁ ≃ₗ[R] N₂) : QuadraticMap R M₁ N₁ ≃ₗ[R] QuadraticMap R M₁ N₂ where - toFun Q := e.compQuadraticMap Q - invFun Q := e.symm.compQuadraticMap Q - left_inv _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] - right_inv _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] - map_add' _ _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, add_apply, map_add, LinearEquiv.coe_coe] - map_smul' _ _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, smul_apply, LinearMapClass.map_smul, - LinearEquiv.coe_coe, RingHom.id_apply] - - variable (R A) in /-- The tensor product of two quadratic maps injects into quadratic maps on tensor products. From 873d58e8215170f6538b66ced634d291dba064b2 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 22 Jul 2024 22:31:30 +0100 Subject: [PATCH 12/49] fudge it into building --- .../BilinearForm/TensorProduct.lean | 5 +++ .../QuadraticForm/TensorProduct.lean | 33 +++++++++++-------- 2 files changed, 24 insertions(+), 14 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index f0cf6f234f9f3..23fcc282b76b3 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -65,6 +65,11 @@ theorem tensorDistrib_tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' := rfl +/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +protected abbrev tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : + BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := + tensorDistrib' R A (B₁ ⊗ₜ[R] B₂) + variable (R A) in /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 684085230778a..ddc36079b0668 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -62,8 +62,8 @@ theorem tensorDistrib_tmul' (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticM /-- The tensor product of two quadratic maps, a shorthand for dot notation. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 -protected noncomputable abbrev tmul' (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) : - QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := +protected noncomputable abbrev _root_.QuadraticMap.tmul' (Q₁ : QuadraticMap A M₁ N₁) + (Q₂ : QuadraticMap R M₂ N₂) : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := tensorDistrib' R A (Q₁ ⊗ₜ[R] Q₂) variable (R A) in @@ -72,9 +72,20 @@ variable (R A) in Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 +-- Should be `(congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A)` but then +-- `associated_tmul` breaks noncomputable def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := - (congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + -- while `letI`s would produce a better term than `let`, they would make this already-slow + -- definition even slower. + let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) + let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + let toB := AlgebraTensorModule.map + (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) + toQ ∘ₗ tmulB ∘ₗ toB +-- -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for -- `R = A` of `Q₁ m₁ * Q₂ m₂`. @@ -91,19 +102,13 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra QuadraticForm A (M₁ ⊗[R] M₂) := tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) -theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) - (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) - = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by sorry -/- - rw [QuadraticMap.tmul, tensorDistrib, tensorDistrib', BilinMap.tmul, congr₂, - AlgebraTensorModule.rid] - simp_rw [LinearMap.compQuadraticMap] - --simp? - dsimp? +theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : + associated (R := A) (Q₁.tmul Q₂) + = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by + rw [QuadraticForm.tmul, tensorDistrib, BilinMap.tmul] + dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) - dsimp only --/ theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • (polarBilin Q₁).tmul (polarBilin Q₂) := by From 13cd0ee1dae7398a8349bedbb2b7db76185aa593 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Tue, 23 Jul 2024 08:05:35 +0100 Subject: [PATCH 13/49] =?UTF-8?q?Implement=20LinearMap.BilinMap.congr?= =?UTF-8?q?=E2=82=82=20with=20LinearEquiv.congrRight?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index ed951ddec61db..c507dd3731338 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -311,19 +311,9 @@ variable [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N /-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear maps into `N₂`. -/ -@[simps] -def _root_.LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ where - toFun B := LinearMap.compr₂ B e - invFun B := LinearMap.compr₂ B e.symm - left_inv B := ext₂ fun x => by - simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, implies_true] - right_inv B := ext₂ fun x => by - simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, implies_true] - map_add' B B' := ext₂ fun x y => by - simp only [compr₂_apply, LinearMap.add_apply, map_add, LinearEquiv.coe_coe] - map_smul' B B' := ext₂ fun x y => by - simp only [compr₂_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe, - RingHom.id_apply] +@[simps!] +def _root_.LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := + LinearEquiv.congrRight (LinearEquiv.congrRight e) end congr From 624ba77e07e573fb6db03b09e7ccbceef5f89a4c Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Tue, 23 Jul 2024 08:24:07 +0100 Subject: [PATCH 14/49] Implement LinearMap.BilinForm.congr with LinearEquiv.congrRight and LinearEquiv.congrLeft --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index c507dd3731338..6957d4f0a43bc 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -262,15 +262,8 @@ variable [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] section congr /-- Apply a linear equivalence on the arguments of a bilinear form. -/ -def congr (e : M ≃ₗ[R] M') : BilinForm R M ≃ₗ[R] BilinForm R M' where - toFun B := B.comp e.symm e.symm - invFun B := B.comp e e - left_inv B := ext₂ fun x => by - simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, forall_const] - right_inv B := ext₂ fun x => by - simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, forall_const] - map_add' B B' := ext₂ fun x y => rfl - map_smul' B B' := ext₂ fun x y => rfl +def congr (e : M ≃ₗ[R] M') : BilinForm R M ≃ₗ[R] BilinForm R M' := + LinearEquiv.congrRight (LinearEquiv.congrLeft _ _ e) ≪≫ₗ LinearEquiv.congrLeft _ _ e @[simp] theorem congr_apply (e : M ≃ₗ[R] M') (B : BilinForm R M) (x y : M') : From 35779ab5af6991fabeeac44c9eb31872ce4c4c28 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Thu, 15 Aug 2024 08:17:36 +0100 Subject: [PATCH 15/49] Remove unused vars --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 67bfff0431c9f..c618fff5332a9 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -31,8 +31,7 @@ section CommRing variable [CommRing R] [CommRing A] variable [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] -variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] -variable [SMulCommClass R A N₁] [SMulCommClass A R N₁] [IsScalarTower R A N₁] +variable [SMulCommClass R A M₁] [IsScalarTower R A M₁] [SMulCommClass R A N₁] [IsScalarTower R A N₁] variable [Module R M₂] [Module R N₂] section InvertibleTwo From 32fae521f318f08cf26a4874feab1ad091cf8f32 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Wed, 2 Oct 2024 19:20:00 +0100 Subject: [PATCH 16/49] Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 34514f581b33e..8c36aefc8d630 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -580,7 +580,7 @@ def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S _root_.LinearMap.compQuadraticMap f Q.restrictScalars -/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear +/-- When `N₁` and `N₂` are equivalent, quadratic maps on `M` into `N₁` are equivalent to quadratic maps into `N₂`. -/ @[simps] def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where From f1095a55d51625376823d1aa7b72b31a5db2cf9e Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Wed, 2 Oct 2024 19:21:30 +0100 Subject: [PATCH 17/49] Correct doc string --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 8c36aefc8d630..c41d3613425b0 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -580,8 +580,8 @@ def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S _root_.LinearMap.compQuadraticMap f Q.restrictScalars -/-- When `N₁` and `N₂` are equivalent, quadratic maps on `M` into `N₁` are equivalent to quadratic -maps into `N₂`. -/ +/-- When `N` and `P` are equivalent, quadratic maps on `M` into `N` are equivalent to quadratic +maps on `M` into `P`. -/ @[simps] def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where toFun Q := e.compQuadraticMap Q From 1b97cd78095ddc2ece018a8aaa5056ea0ed98cb4 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Wed, 2 Oct 2024 19:25:37 +0100 Subject: [PATCH 18/49] Remove spurious -- --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 0ae8cd40d3da0..020d1b708949b 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -85,7 +85,6 @@ noncomputable def tensorDistrib : (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) toQ ∘ₗ tmulB ∘ₗ toB --- -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for -- `R = A` of `Q₁ m₁ * Q₂ m₂`. From da9154a379ba603fccaaba6dab53646407704e73 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Thu, 3 Oct 2024 02:55:14 +0100 Subject: [PATCH 19/49] Add docstrings --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 1 + Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 14fe1eb416257..d212483dc8acb 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -57,6 +57,7 @@ def tensorDistrib' : (TensorProduct.lift.equiv A M₁ M₁ N₁) (TensorProduct.lift.equiv R _ _ _)).toLinearMap +/-- The name `tensorDistrib_tmul` is taken by the `BilinForm` version of this result -/ @[simp] theorem tensorDistrib_tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 020d1b708949b..31cfd8ebedb7c 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -53,6 +53,7 @@ noncomputable def tensorDistrib' : (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) toQ ∘ₗ tmulB ∘ₗ toB +/-- The name `tensorDistrib_tmul` is taken by the `QuadraticForm` version of this result -/ @[simp] theorem tensorDistrib_tmul' (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) : tensorDistrib' R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := From 390c528fce19944427ccd107f4e47fcc0285a2b8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 5 Oct 2024 14:17:55 +0000 Subject: [PATCH 20/49] deprecate and change name --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 8e02a6129e3c3..17c90f3995c20 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -902,7 +902,7 @@ instance canLift : /-- There exists a non-null vector with respect to any quadratic form `Q` whose associated bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`. -/ -theorem exists_quadraticForm_ne_zero {Q : QuadraticMap R M N} +theorem exists_quadraticMap_ne_zero {Q : QuadraticMap R M N} -- Porting note: added implicit argument (hB₁ : associated' (R := R) (N := N) Q ≠ 0) : ∃ x, Q x ≠ 0 := by @@ -911,6 +911,9 @@ theorem exists_quadraticForm_ne_zero {Q : QuadraticMap R M N} apply hB₁ rw [(QuadraticMap.ext h : Q = 0), LinearMap.map_zero] +@[deprecated (since := "2024-10-05")] alias exists_quadraticForm_ne_zero := + exists_quadraticMap_ne_zero + end AssociatedHom section Associated From 85c9ca419890d9ab1effb38109e6be259259380d Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 5 Oct 2024 20:50:18 +0100 Subject: [PATCH 21/49] Fix --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 17c90f3995c20..0ad0ba5eb6ca0 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -1197,7 +1197,7 @@ on a module `M` over a ring `R` with invertible `2`, i.e. there exists some theorem exists_bilinForm_self_ne_zero [htwo : Invertible (2 : R)] {B : BilinForm R M} (hB₁ : B ≠ 0) (hB₂ : B.IsSymm) : ∃ x, ¬B.IsOrtho x x := by lift B to QuadraticForm R M using hB₂ with Q - obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticForm_ne_zero hB₁ + obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁ exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩ open Module From e03280802e45756383414af3d3245710dbe00f1b Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 5 Oct 2024 20:59:51 +0100 Subject: [PATCH 22/49] =?UTF-8?q?QuadraticMap.congr=E2=82=82?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index fe2fe2b66dfe2..a334da8731f85 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -579,6 +579,22 @@ def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S (f : N →ₗ[S] P) (Q : QuadraticMap R M N) : QuadraticMap S M P := _root_.LinearMap.compQuadraticMap f Q.restrictScalars +/-- When `N` and `P` are equivalent, quadratic maps on `M` into `N` are equivalent to quadratic +maps on `M` into `P`. -/ +@[simps] +def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where + toFun Q := e.compQuadraticMap Q + invFun Q := e.symm.compQuadraticMap Q + left_inv _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] + right_inv _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] + map_add' _ _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, add_apply, map_add, LinearEquiv.coe_coe] + map_smul' _ _ := ext fun x => by + simp only [LinearMap.compQuadraticMap_apply, smul_apply, LinearMapClass.map_smul, + LinearEquiv.coe_coe, RingHom.id_apply] + end Comp section NonUnitalNonAssocSemiring From d2ec91876c60d35e663c9474fa6b77c7046dd4bd Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 5 Oct 2024 21:05:13 +0100 Subject: [PATCH 23/49] =?UTF-8?q?LinearMap.BilinMap.congr=E2=82=82?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index f32f28e8aea31..f0b0bc5dc6a02 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -39,6 +39,7 @@ Bilinear form, -/ open LinearMap (BilinForm) +open LinearMap (BilinMap) universe u v w @@ -305,6 +306,15 @@ theorem comp_congr (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l r : M' →ₗ[R B.comp (l.comp (e.symm : M'' →ₗ[R] M')) (r.comp (e.symm : M'' →ₗ[R] M')) := rfl +variable {N₁ N₂ : Type*} +variable [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] + +/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear +maps into `N₂`. -/ +@[simps!] +def _root_.LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := + LinearEquiv.congrRight (LinearEquiv.congrRight e) + end congr section LinMulLin From 3b08310b2873ec0b87c6462fbf7ce15e48cfd724 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 5 Oct 2024 21:31:06 +0100 Subject: [PATCH 24/49] =?UTF-8?q?congr=E2=82=82=5Frefl=20and=20congr?= =?UTF-8?q?=E2=82=82=5Fsymm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index a334da8731f85..faeca7b1ca5ea 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -595,6 +595,11 @@ def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M simp only [LinearMap.compQuadraticMap_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe, RingHom.id_apply] +@[simp] +theorem congr₂_refl : congr₂ (.refl R N) = .refl R (QuadraticMap R M N) := rfl + +theorem congr₂_symm (e : N ≃ₗ[R] P) : congr₂ e.symm = (congr₂ e (M := M)).symm := rfl + end Comp section NonUnitalNonAssocSemiring From d22d812ad3aa664c89ff13999933f59342611f8f Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 5 Oct 2024 22:27:28 +0100 Subject: [PATCH 25/49] Rename --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index faeca7b1ca5ea..f0a38a38bd1e6 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -582,7 +582,8 @@ def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S /-- When `N` and `P` are equivalent, quadratic maps on `M` into `N` are equivalent to quadratic maps on `M` into `P`. -/ @[simps] -def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where +def _root_.LinearEquiv.congrQuadraticMap (e : N ≃ₗ[R] P) : + QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where toFun Q := e.compQuadraticMap Q invFun Q := e.symm.compQuadraticMap Q left_inv _ := ext fun x => by @@ -596,9 +597,11 @@ def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M LinearEquiv.coe_coe, RingHom.id_apply] @[simp] -theorem congr₂_refl : congr₂ (.refl R N) = .refl R (QuadraticMap R M N) := rfl +theorem congr₂_refl : + LinearEquiv.congrQuadraticMap (.refl R N) = .refl R (QuadraticMap R M N) := rfl -theorem congr₂_symm (e : N ≃ₗ[R] P) : congr₂ e.symm = (congr₂ e (M := M)).symm := rfl +theorem congr₂_symm (e : N ≃ₗ[R] P) : LinearEquiv.congrQuadraticMap e.symm = + (LinearEquiv.congrQuadraticMap e (M := M)).symm := rfl end Comp section NonUnitalNonAssocSemiring From 02c2c5aa8165f86334088d9677a4fd556367334f Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 5 Oct 2024 22:29:09 +0100 Subject: [PATCH 26/49] Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index f0a38a38bd1e6..c9e19db04b58a 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -601,7 +601,7 @@ theorem congr₂_refl : LinearEquiv.congrQuadraticMap (.refl R N) = .refl R (QuadraticMap R M N) := rfl theorem congr₂_symm (e : N ≃ₗ[R] P) : LinearEquiv.congrQuadraticMap e.symm = - (LinearEquiv.congrQuadraticMap e (M := M)).symm := rfl + (LinearEquiv.congrQuadraticMap e (M := M)).symm := rfl end Comp section NonUnitalNonAssocSemiring From 1e125a364d7e4978bf270247124ef929be12d1cf Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sun, 6 Oct 2024 05:24:42 +0100 Subject: [PATCH 27/49] =?UTF-8?q?Add=20congr=E2=82=82=20section?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index f0b0bc5dc6a02..c47eba3152378 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -306,16 +306,27 @@ theorem comp_congr (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l r : M' →ₗ[R B.comp (l.comp (e.symm : M'' →ₗ[R] M')) (r.comp (e.symm : M'' →ₗ[R] M')) := rfl +end congr + +section congr₂ + variable {N₁ N₂ : Type*} variable [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] /-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear maps into `N₂`. -/ @[simps!] -def _root_.LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := +def LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := LinearEquiv.congrRight (LinearEquiv.congrRight e) -end congr +@[simp] +theorem congr₂_refl : + LinearMap.BilinMap.congr₂ (.refl R N₁) = .refl R (BilinMap R M N₁) := rfl + +theorem congr₂_symm (e : N₁ ≃ₗ[R] N₂) : LinearMap.BilinMap.congr₂ e.symm = + (LinearMap.BilinMap.congr₂ e (M := M)).symm := rfl + +end congr₂ section LinMulLin From 6cd85c3630b09bf3b0087cb0918b65ffd9fd6a62 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 6 Oct 2024 12:12:05 +0000 Subject: [PATCH 28/49] tidy --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 21 ++++++++++++---- .../LinearAlgebra/QuadraticForm/Basic.lean | 24 +++++++++---------- 2 files changed, 27 insertions(+), 18 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index c47eba3152378..d8b74cb6f7bf2 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -310,21 +310,32 @@ end congr section congr₂ -variable {N₁ N₂ : Type*} -variable [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] +variable {N₁ N₂ N₃ : Type*} +variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] +variable [Module R N₁] [Module R N₂] [Module R N₃] /-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear maps into `N₂`. -/ -@[simps!] def LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := LinearEquiv.congrRight (LinearEquiv.congrRight e) +@[simp] +theorem LinearMap.BilinMap.congr₂_apply (e : N₁ ≃ₗ[R] N₂) (B : BilinMap R M N₁) : + LinearMap.BilinMap.congr₂ e B = compr₂ B e := rfl + @[simp] theorem congr₂_refl : LinearMap.BilinMap.congr₂ (.refl R N₁) = .refl R (BilinMap R M N₁) := rfl -theorem congr₂_symm (e : N₁ ≃ₗ[R] N₂) : LinearMap.BilinMap.congr₂ e.symm = - (LinearMap.BilinMap.congr₂ e (M := M)).symm := rfl +@[simp] +theorem congr₂_symm (e : N₁ ≃ₗ[R] N₂) : + (LinearMap.BilinMap.congr₂ e (M := M)).symm = LinearMap.BilinMap.congr₂ e.symm := + rfl + +theorem congr₂_trans (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) : + LinearMap.BilinMap.congr₂ (M := M) (e₁₂ ≪≫ₗ e₂₃) = + LinearMap.BilinMap.congr₂ e₁₂ ≪≫ₗ LinearMap.BilinMap.congr₂ e₂₃ := + rfl end congr₂ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index c9e19db04b58a..002a39d360675 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -580,28 +580,26 @@ def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S _root_.LinearMap.compQuadraticMap f Q.restrictScalars /-- When `N` and `P` are equivalent, quadratic maps on `M` into `N` are equivalent to quadratic -maps on `M` into `P`. -/ +maps on `M` into `P`. + +See `LinearMap.BilinMap.congr₂` for the bilinear map version. -/ @[simps] def _root_.LinearEquiv.congrQuadraticMap (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where toFun Q := e.compQuadraticMap Q invFun Q := e.symm.compQuadraticMap Q - left_inv _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] - right_inv _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] - map_add' _ _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, add_apply, map_add, LinearEquiv.coe_coe] - map_smul' _ _ := ext fun x => by - simp only [LinearMap.compQuadraticMap_apply, smul_apply, LinearMapClass.map_smul, - LinearEquiv.coe_coe, RingHom.id_apply] + left_inv _ := ext fun _ => e.symm_apply_apply _ + right_inv _ := ext fun _ => e.apply_symm_apply _ + map_add' _ _ := ext fun _ => map_add e _ _ + map_smul' _ _ := ext fun _ => _root_.map_smul e _ _ @[simp] -theorem congr₂_refl : +theorem _root_.LinearEquiv.congrQuadraticMap_refl : LinearEquiv.congrQuadraticMap (.refl R N) = .refl R (QuadraticMap R M N) := rfl -theorem congr₂_symm (e : N ≃ₗ[R] P) : LinearEquiv.congrQuadraticMap e.symm = - (LinearEquiv.congrQuadraticMap e (M := M)).symm := rfl +@[simp] +theorem _root_.LinearEquiv.congrQuadraticMap_symm (e : N ≃ₗ[R] P) : + (LinearEquiv.congrQuadraticMap e (M := M)).symm = e.symm.congrQuadraticMap := rfl end Comp section NonUnitalNonAssocSemiring From 6e990d832b0560c39cccb375b84e86c38665585c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 6 Oct 2024 12:13:50 +0000 Subject: [PATCH 29/49] fix double-namespace --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index d8b74cb6f7bf2..d350a545416cf 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -316,25 +316,24 @@ variable [Module R N₁] [Module R N₂] [Module R N₃] /-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear maps into `N₂`. -/ -def LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := +def congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := LinearEquiv.congrRight (LinearEquiv.congrRight e) @[simp] -theorem LinearMap.BilinMap.congr₂_apply (e : N₁ ≃ₗ[R] N₂) (B : BilinMap R M N₁) : - LinearMap.BilinMap.congr₂ e B = compr₂ B e := rfl +theorem congr₂_apply (e : N₁ ≃ₗ[R] N₂) (B : BilinMap R M N₁) : + congr₂ e B = compr₂ B e := rfl @[simp] theorem congr₂_refl : - LinearMap.BilinMap.congr₂ (.refl R N₁) = .refl R (BilinMap R M N₁) := rfl + congr₂ (.refl R N₁) = .refl R (BilinMap R M N₁) := rfl @[simp] theorem congr₂_symm (e : N₁ ≃ₗ[R] N₂) : - (LinearMap.BilinMap.congr₂ e (M := M)).symm = LinearMap.BilinMap.congr₂ e.symm := + (congr₂ e (M := M)).symm = congr₂ e.symm := rfl theorem congr₂_trans (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) : - LinearMap.BilinMap.congr₂ (M := M) (e₁₂ ≪≫ₗ e₂₃) = - LinearMap.BilinMap.congr₂ e₁₂ ≪≫ₗ LinearMap.BilinMap.congr₂ e₂₃ := + congr₂ (M := M) (e₁₂ ≪≫ₗ e₂₃) = congr₂ e₁₂ ≪≫ₗ congr₂ e₂₃ := rfl end congr₂ From 15213e8620846d30c0b164045f83f3a70b6c7cd7 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 14 Oct 2024 19:02:09 +0100 Subject: [PATCH 30/49] Fix --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index 5c0bf079aeed7..2a585b15e9678 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -1,4 +1,4 @@ - /- +/- Copyright (c) 2018 Andreas Swerdlow. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andreas Swerdlow, Kexing Ying @@ -316,6 +316,7 @@ variable {N₁ N₂ N₃ : Type*} variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] variable [Module R N₁] [Module R N₂] [Module R N₃] +#check LinearMap /-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear maps into `N₂`. -/ def congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := From 6a8d38b97924dfaab19ef1a37b503bb92dbc96c9 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 14 Oct 2024 19:26:46 +0100 Subject: [PATCH 31/49] Gah --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index 2a585b15e9678..e6f3bcda0c271 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -316,7 +316,6 @@ variable {N₁ N₂ N₃ : Type*} variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] variable [Module R N₁] [Module R N₂] [Module R N₃] -#check LinearMap /-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear maps into `N₂`. -/ def congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := From 4133bb30ae0e5b5a1f92206edc26b371e4846e2c Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Thu, 24 Oct 2024 07:33:18 +0100 Subject: [PATCH 32/49] Remove duplicate def --- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 9 --------- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 2 +- 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index 8eb381dc5750e..9c011c36ed52b 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -299,15 +299,6 @@ theorem comp_congr (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l r : M' →ₗ[R B.comp (l.comp (e.symm : M'' →ₗ[R] M')) (r.comp (e.symm : M'' →ₗ[R] M')) := rfl -variable {N₁ N₂ : Type*} -variable [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] - -/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear -maps into `N₂`. -/ -@[simps!] -def _root_.LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ := - LinearEquiv.congrRight (LinearEquiv.congrRight e) - end congr section congrRight₂ diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index d212483dc8acb..c5b0c815de129 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -76,7 +76,7 @@ variable (R A) in Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra over the ring in which the right bilinear form is valued. -/ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - (congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) + (LinearEquiv.congrRight₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) variable (R A) in From d75ee5bd49b6bd9dca5f5d922ae8bc739f0b607d Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Thu, 24 Oct 2024 07:40:03 +0100 Subject: [PATCH 33/49] Dot notation --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index c5b0c815de129..836a07d5456aa 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -76,7 +76,7 @@ variable (R A) in Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra over the ring in which the right bilinear form is valued. -/ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - (LinearEquiv.congrRight₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A) + (AlgebraTensorModule.rid R A A).congrRight₂.toLinearMap ∘ₗ (tensorDistrib' R A) variable (R A) in From cd7de904d46158c2f1a1aca0b2d6904437363cb5 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Fri, 25 Oct 2024 20:10:08 +0100 Subject: [PATCH 34/49] Update Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean Co-authored-by: Eric Wieser --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 836a07d5456aa..97675af41abee 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -48,7 +48,7 @@ variable (R A) in Note this is heterobasic; the bilinear map on the left can take values in a module over a (commutative) algebra over the ring of the module in which the right bilinear map is valued. -/ def tensorDistrib' : - ((BilinMap A M₁ N₁) ⊗[R] (BilinMap R M₂ N₂)) →ₗ[A] ((BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))) := + (BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ ((LinearMap.llcomp A _ _ _).flip (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap) From 3e25ca45fb10208e5ab89f7cbd79ff48c182d7c3 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Fri, 25 Oct 2024 22:20:00 +0100 Subject: [PATCH 35/49] Rename --- .../BilinearForm/TensorProduct.lean | 39 ++++++++++------ .../QuadraticForm/TensorProduct.lean | 46 ++++++++++--------- 2 files changed, 49 insertions(+), 36 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 97675af41abee..2331b16d130a6 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -30,11 +30,10 @@ open TensorProduct namespace LinearMap -namespace BilinMap - open LinearMap (BilinMap BilinForm) section CommSemiring + variable [CommSemiring R] [CommSemiring A] variable [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] @@ -42,12 +41,14 @@ variable [SMulCommClass R A M₁] [IsScalarTower R A M₁] variable [SMulCommClass R A N₁] [IsScalarTower R A N₁] variable [Module R M₂] [Module R N₂] +namespace BilinMap + variable (R A) in /-- The tensor product of two bilinear maps injects into bilinear maps on tensor products. Note this is heterobasic; the bilinear map on the left can take values in a module over a (commutative) algebra over the ring of the module in which the right bilinear map is valued. -/ -def tensorDistrib' : +def tensorDistrib : (BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ ((LinearMap.llcomp A _ _ _).flip @@ -59,16 +60,20 @@ def tensorDistrib' : /-- The name `tensorDistrib_tmul` is taken by the `BilinForm` version of this result -/ @[simp] -theorem tensorDistrib_tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensorDistrib' R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' := rfl /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -protected abbrev tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : +protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := - tensorDistrib' R A (B₁ ⊗ₜ[R] B₂) + tensorDistrib R A (B₁ ⊗ₜ[R] B₂) + +end BilinMap + +namespace BilinForm variable (R A) in /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. @@ -76,7 +81,7 @@ variable (R A) in Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra over the ring in which the right bilinear form is valued. -/ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := - (AlgebraTensorModule.rid R A A).congrRight₂.toLinearMap ∘ₗ (tensorDistrib' R A) + (AlgebraTensorModule.rid R A A).congrRight₂.toLinearMap ∘ₗ (BilinMap.tensorDistrib R A) variable (R A) in @@ -90,12 +95,12 @@ theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) ( rfl /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -protected abbrev tmul (B₁ : BilinMap A M₁ A) (B₂ : BilinMap R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A := +protected abbrev tmul (B₁ : BilinForm A M₁) (B₂ : BilinMap R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A := tensorDistrib R A (B₁ ⊗ₜ[R] B₂) attribute [local ext] TensorProduct.ext in /-- A tensor product of symmetric bilinear forms is symmetric. -/ -lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R M₂ R} +lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by rw [LinearMap.isSymm_iff_eq_flip] ext x₁ x₂ y₁ y₂ @@ -103,11 +108,11 @@ lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R variable (A) in /-- The base change of a bilinear form. -/ -protected def baseChange (B : BilinMap R M₂ R) : BilinForm A (A ⊗[R] M₂) := - BilinMap.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B +protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := + BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B @[simp] -theorem baseChange_tmul (B₂ : BilinMap R M₂ R) (a : A) (m₂ : M₂) +theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := rfl @@ -117,6 +122,8 @@ variable (A) in lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm := IsSymm.tmul mul_comm hB₂ +end BilinForm + end CommSemiring section CommRing @@ -127,6 +134,8 @@ variable [Module R M₁] [Module R M₂] variable [Module.Free R M₁] [Module.Finite R M₁] variable [Module.Free R M₂] [Module.Finite R M₂] +namespace BilinForm + variable (R) in /-- `tensorDistrib` as an equivalence. -/ noncomputable def tensorDistribEquiv : @@ -159,8 +168,8 @@ theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B := DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B -end CommRing +end BilinForm -end BilinMap +end CommRing end LinearMap diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 31cfd8ebedb7c..ef5381d8cda9e 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -23,8 +23,6 @@ variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N open LinearMap (BilinMap BilinForm) open TensorProduct QuadraticMap -namespace QuadraticForm - section CommRing variable [CommRing R] [CommRing A] variable [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] @@ -35,19 +33,21 @@ variable [Module R M₂] [Module R N₂] section InvertibleTwo variable [Invertible (2 : R)] +namespace QuadraticMap + variable (R A) in /-- The tensor product of two quadratic maps injects into quadratic maps on tensor products. Note this is heterobasic; the quadratic map on the left can take values in a module over a larger ring than the one on the right. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 -noncomputable def tensorDistrib' : +noncomputable def tensorDistrib : QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm -- while `letI`s would produce a better term than `let`, they would make this already-slow -- definition even slower. let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) - let tmulB := BilinMap.tensorDistrib' R A (M₁ := M₁) (M₂ := M₂) + let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map (QuadraticMap.associated : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁) (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) @@ -55,17 +55,21 @@ noncomputable def tensorDistrib' : /-- The name `tensorDistrib_tmul` is taken by the `QuadraticForm` version of this result -/ @[simp] -theorem tensorDistrib_tmul' (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) - (m₂ : M₂) : tensorDistrib' R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := +theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) + (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - (BilinMap.tensorDistrib_tmul' _ _ _ _ _ _).trans <| congr_arg₂ _ + (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic maps, a shorthand for dot notation. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 -protected noncomputable abbrev _root_.QuadraticMap.tmul' (Q₁ : QuadraticMap A M₁ N₁) +protected noncomputable abbrev tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := - tensorDistrib' R A (Q₁ ⊗ₜ[R] Q₂) + tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) + +end QuadraticMap + +namespace QuadraticForm variable (R A) in /-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. @@ -81,7 +85,7 @@ noncomputable def tensorDistrib : -- while `letI`s would produce a better term than `let`, they would make this already-slow -- definition even slower. let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) - let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) @@ -93,7 +97,7 @@ noncomputable def tensorDistrib : theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - (BilinMap.tensorDistrib_tmul _ _ _ _ _ _ _ _).trans <| congr_arg₂ _ + (LinearMap.BilinForm.tensorDistrib_tmul _ _ _ _ _ _ _ _).trans <| congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ @@ -103,16 +107,16 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : - associated (R := A) (Q₁.tmul Q₂) - = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by - rw [QuadraticForm.tmul, tensorDistrib, BilinMap.tmul] + associated (R := A) (N := A) (Q₁.tmul Q₂) + = BilinForm.tmul ((associated (R := A) (N := A) Q₁)) (associated (R := R) (N := R) Q₂) := by + rw [QuadraticForm.tmul, tensorDistrib, BilinForm.tmul] dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : - polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • (polarBilin Q₁).tmul (polarBilin Q₂) := by - simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinMap.tmul, tmul_smul, + polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • BilinForm.tmul (polarBilin Q₁) (polarBilin Q₂) := by + simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinForm.tmul, tmul_smul, ← smul_tmul', map_nsmul, associated_tmul] rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two, one_smul] @@ -129,17 +133,19 @@ theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : tensorDistrib_tmul _ _ _ _ theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : - associated (R := A) (Q.baseChange A) = (associated (R := R) Q).baseChange A := by + associated (R := A) (Q.baseChange A) = BilinForm.baseChange A (associated (R := R) Q) := by dsimp only [QuadraticForm.baseChange, LinearMap.baseChange] rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq] exact rfl theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : - polarBilin (Q.baseChange A) = (polarBilin Q).baseChange A := by - rw [QuadraticForm.baseChange, BilinMap.baseChange, polarBilin_tmul, BilinMap.tmul, + polarBilin (Q.baseChange A) = BilinForm.baseChange A (polarBilin Q) := by + rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul, ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq, smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul] +end QuadraticForm + end InvertibleTwo /-- If two quadratic forms from `A ⊗[R] M₂` agree on elements of the form `1 ⊗ m`, they are equal. @@ -167,5 +173,3 @@ theorem baseChange_ext ⦃Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)⦄ linear_combination this + hx + hy end CommRing - -end QuadraticForm From 6f0e4a2505ad6551382483a453a5a258dbbcaf70 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Fri, 25 Oct 2024 22:22:33 +0100 Subject: [PATCH 36/49] Remove old docstring --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 2331b16d130a6..65142b528a58a 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -58,7 +58,6 @@ def tensorDistrib : (TensorProduct.lift.equiv A M₁ M₁ N₁) (TensorProduct.lift.equiv R _ _ _)).toLinearMap -/-- The name `tensorDistrib_tmul` is taken by the `BilinForm` version of this result -/ @[simp] theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : From ededa785cc5ddf7c8b9530a0273641ba65b2bde7 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Fri, 25 Oct 2024 22:25:13 +0100 Subject: [PATCH 37/49] Remove old docstring --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index ef5381d8cda9e..bc0230005ad37 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -53,7 +53,6 @@ noncomputable def tensorDistrib : (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) toQ ∘ₗ tmulB ∘ₗ toB -/-- The name `tensorDistrib_tmul` is taken by the `QuadraticForm` version of this result -/ @[simp] theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂ := From de320350ce372d914c2f8037733aebbf4628da23 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Fri, 25 Oct 2024 22:36:04 +0100 Subject: [PATCH 38/49] Update comment --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index bc0230005ad37..c1fb219072942 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -76,8 +76,9 @@ variable (R A) in Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 --- Should be `(congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A)` but then --- `associated_tmul` breaks +-- Should be +-- `(AlgebraTensorModule.rid R A A).congrQuadraticMap.toLinearMap ∘ₗ QuadraticMap.tensorDistrib R A` +-- but then `associated_tmul` breaks noncomputable def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm From 1677ddcd2eaeb1dd3e9962c6c6b5dddbe80da2c6 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Fri, 25 Oct 2024 22:47:00 +0100 Subject: [PATCH 39/49] Fix --- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index e83ba0a051353..e25b22b5361e7 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -95,7 +95,7 @@ noncomputable def toBaseChange (Q : QuadraticForm R V) : exact hpure_tensor v w intros v w rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap, - QuadraticForm.polarBilin_baseChange, LinearMap.BilinMap.baseChange_tmul, one_mul, + QuadraticForm.polarBilin_baseChange, LinearMap.BilinForm.baseChange_tmul, one_mul, TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticMap.polarBilin_apply_apply] @[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) : From 18b17e9768a8e1ec5b8dad55a3e3350cbe45d49b Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Fri, 25 Oct 2024 22:50:03 +0100 Subject: [PATCH 40/49] Simplify --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index c1fb219072942..5ecdb2b4c48c2 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -107,8 +107,8 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : - associated (R := A) (N := A) (Q₁.tmul Q₂) - = BilinForm.tmul ((associated (R := A) (N := A) Q₁)) (associated (R := R) (N := R) Q₂) := by + associated (R := A) (Q₁.tmul Q₂) + = BilinForm.tmul ((associated (R := A) Q₁)) (associated (R := R) Q₂) := by rw [QuadraticForm.tmul, tensorDistrib, BilinForm.tmul] dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance From 7823fa36e71b5bc1bd9a05eefa13e2855e16f223 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 26 Oct 2024 06:29:11 +0100 Subject: [PATCH 41/49] Update Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean Co-authored-by: Eric Wieser --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 65142b528a58a..71c67074e7f0e 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -66,7 +66,7 @@ theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ rfl /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ -protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : +protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) : BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := tensorDistrib R A (B₁ ⊗ₜ[R] B₂) From 0402b3040b9560d7b47b979d9f9ab7b77b18e1e7 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 26 Oct 2024 07:02:32 +0100 Subject: [PATCH 42/49] Try new QuadraticForm.tensorDistrib def --- .../LinearAlgebra/QuadraticForm/TensorProduct.lean | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 5ecdb2b4c48c2..929afed5919c1 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -76,20 +76,9 @@ variable (R A) in Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right. -/ -- `noncomputable` is a performance workaround for mathlib4#7103 --- Should be --- `(AlgebraTensorModule.rid R A A).congrQuadraticMap.toLinearMap ∘ₗ QuadraticMap.tensorDistrib R A` --- but then `associated_tmul` breaks noncomputable def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := - letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - -- while `letI`s would produce a better term than `let`, they would make this already-slow - -- definition even slower. - let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) - let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) - let toB := AlgebraTensorModule.map - (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) - toQ ∘ₗ tmulB ∘ₗ toB + (AlgebraTensorModule.rid R A A).congrQuadraticMap.toLinearMap ∘ₗ QuadraticMap.tensorDistrib R A -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for -- `R = A` of `Q₁ m₁ * Q₂ m₂`. From 90ed818f5d1e3967ee2ccd9c0e1739bf28fc6496 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 26 Oct 2024 07:15:23 +0100 Subject: [PATCH 43/49] Patch it back together --- .../QuadraticForm/TensorProduct.lean | 30 ++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 929afed5919c1..10005dcf7f2d3 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -95,10 +95,38 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra QuadraticForm A (M₁ ⊗[R] M₂) := tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) +variable (R A) in +/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. + +Note this is heterobasic; the quadratic form on the left can take values in a larger ring than +the one on the right. -/ +-- `noncomputable` is a performance workaround for mathlib4#7103 +noncomputable def tensorDistrib' : + QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + -- while `letI`s would produce a better term than `let`, they would make this already-slow + -- definition even slower. + let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) + let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + let toB := AlgebraTensorModule.map + (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) + toQ ∘ₗ tmulB ∘ₗ toB + +/-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ +-- `noncomputable` is a performance workaround for mathlib4#7103 +protected noncomputable abbrev tmul' (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : + QuadraticForm A (M₁ ⊗[R] M₂) := + tensorDistrib' R A (Q₁ ⊗ₜ[R] Q₂) + +lemma helper [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : + (Q₁.tmul' Q₂) = (Q₁.tmul Q₂) := by aesop + theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) = BilinForm.tmul ((associated (R := A) Q₁)) (associated (R := R) Q₂) := by - rw [QuadraticForm.tmul, tensorDistrib, BilinForm.tmul] + simp_rw [← helper] + rw [QuadraticForm.tmul', tensorDistrib', BilinForm.tmul] dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) From a67361e272d42647d02260fe54e0d598e9e115c0 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 26 Oct 2024 07:42:22 +0100 Subject: [PATCH 44/49] Remove unused argument --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 10005dcf7f2d3..2893095fe8342 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -119,7 +119,7 @@ protected noncomputable abbrev tmul' (Q₁ : QuadraticForm A M₁) (Q₂ : Quadr QuadraticForm A (M₁ ⊗[R] M₂) := tensorDistrib' R A (Q₁ ⊗ₜ[R] Q₂) -lemma helper [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : +lemma helper (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : (Q₁.tmul' Q₂) = (Q₁.tmul Q₂) := by aesop theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : From 1ebaabde95a407514ba56f74197b0753132ca002 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 26 Oct 2024 19:26:37 +0100 Subject: [PATCH 45/49] Improve --- .../LinearAlgebra/QuadraticForm/TensorProduct.lean | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 2893095fe8342..1abcc2c88d727 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -113,20 +113,12 @@ noncomputable def tensorDistrib' : (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) toQ ∘ₗ tmulB ∘ₗ toB -/-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ --- `noncomputable` is a performance workaround for mathlib4#7103 -protected noncomputable abbrev tmul' (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : - QuadraticForm A (M₁ ⊗[R] M₂) := - tensorDistrib' R A (Q₁ ⊗ₜ[R] Q₂) - -lemma helper (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : - (Q₁.tmul' Q₂) = (Q₁.tmul Q₂) := by aesop +lemma helper2 : tensorDistrib' = tensorDistrib := rfl theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) = BilinForm.tmul ((associated (R := A) Q₁)) (associated (R := R) Q₂) := by - simp_rw [← helper] - rw [QuadraticForm.tmul', tensorDistrib', BilinForm.tmul] + rw [QuadraticForm.tmul, ← helper2, tensorDistrib', BilinForm.tmul] dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) From ab075998fc826e6af8aa1aea63ec135ff5e16d6e Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 26 Oct 2024 19:35:43 +0100 Subject: [PATCH 46/49] Remove alternative def --- .../QuadraticForm/TensorProduct.lean | 29 +++++-------------- 1 file changed, 8 insertions(+), 21 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 1abcc2c88d727..ec2a4443faf81 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -95,30 +95,17 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra QuadraticForm A (M₁ ⊗[R] M₂) := tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) -variable (R A) in -/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. - -Note this is heterobasic; the quadratic form on the left can take values in a larger ring than -the one on the right. -/ --- `noncomputable` is a performance workaround for mathlib4#7103 -noncomputable def tensorDistrib' : - QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := - letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - -- while `letI`s would produce a better term than `let`, they would make this already-slow - -- definition even slower. - let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) - let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) - let toB := AlgebraTensorModule.map - (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) - toQ ∘ₗ tmulB ∘ₗ toB - -lemma helper2 : tensorDistrib' = tensorDistrib := rfl - theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) = BilinForm.tmul ((associated (R := A) Q₁)) (associated (R := R) Q₂) := by - rw [QuadraticForm.tmul, ← helper2, tensorDistrib', BilinForm.tmul] + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + have e1: (BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) ∘ + BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) ∘ + AlgebraTensorModule.map + (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂)) = + tensorDistrib R A := rfl + rw [QuadraticForm.tmul, ← e1, BilinForm.tmul] dsimp have : Subsingleton (Invertible (2 : A)) := inferInstance convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) From 2e3f58796a0d5472a175dcd9fb55947dd74e61fa Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 26 Oct 2024 20:01:11 +0100 Subject: [PATCH 47/49] BilinMap versions of baseChange and baseChange_tmul --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 71c67074e7f0e..5b0fb0f4e2877 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -70,6 +70,17 @@ protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂ BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := tensorDistrib R A (B₁ ⊗ₜ[R] B₂) +variable (A) in +/-- The base change of a bilinear map (also known as "extension of scalars"). -/ +protected def baseChange (B : BilinMap R M₂ N₂) : BilinMap A (A ⊗[R] M₂) (A ⊗[R] N₂) := + BilinMap.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B + +@[simp] +theorem baseChange_tmul (B₂ : BilinMap R M₂ N₂) (a : A) (m₂ : M₂) + (a' : A) (m₂' : M₂) : + B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') ⊗ₜ (B₂ m₂ m₂') := + rfl + end BilinMap namespace BilinForm From 7900d6277eed1180633654e8c631990250e9c544 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 28 Oct 2024 04:27:00 +0000 Subject: [PATCH 48/49] Add explanitory note --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index ec2a4443faf81..a0b0bf546df63 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -95,6 +95,13 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra QuadraticForm A (M₁ ⊗[R] M₂) := tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) +/- Previously `QuadraticForm.tensorDistrib` was defined in a similar way to +`QuadraticMap.tensorDistrib`. We now obtain the definition of `QuadraticForm.tensorDistrib` +from `QuadraticMap.tensorDistrib` using `A ⊗[R] R ≃ₗ[A] A`. Hypothesis `e1` below shows that the +new definition is equal to the old, and allows us to reuse the old proof. + +TODO: Define `IsSymm` for bilinear maps and generalise this result to Quadratic Maps. +-/ theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) = BilinForm.tmul ((associated (R := A) Q₁)) (associated (R := R) Q₂) := by From 21ea33a91244e12a42eeca8cd7e2a0566cc7247e Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 28 Oct 2024 17:54:25 +0000 Subject: [PATCH 49/49] Move comment --- .../LinearAlgebra/QuadraticForm/TensorProduct.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index a0b0bf546df63..48cee02f8f77e 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -95,17 +95,17 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra QuadraticForm A (M₁ ⊗[R] M₂) := tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) -/- Previously `QuadraticForm.tensorDistrib` was defined in a similar way to -`QuadraticMap.tensorDistrib`. We now obtain the definition of `QuadraticForm.tensorDistrib` -from `QuadraticMap.tensorDistrib` using `A ⊗[R] R ≃ₗ[A] A`. Hypothesis `e1` below shows that the -new definition is equal to the old, and allows us to reuse the old proof. - -TODO: Define `IsSymm` for bilinear maps and generalise this result to Quadratic Maps. --/ theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : associated (R := A) (Q₁.tmul Q₂) = BilinForm.tmul ((associated (R := A) Q₁)) (associated (R := R) Q₂) := by letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + /- Previously `QuadraticForm.tensorDistrib` was defined in a similar way to + `QuadraticMap.tensorDistrib`. We now obtain the definition of `QuadraticForm.tensorDistrib` + from `QuadraticMap.tensorDistrib` using `A ⊗[R] R ≃ₗ[A] A`. Hypothesis `e1` below shows that the + new definition is equal to the old, and allows us to reuse the old proof. + + TODO: Define `IsSymm` for bilinear maps and generalise this result to Quadratic Maps. + -/ have e1: (BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) ∘ BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) ∘ AlgebraTensorModule.map