From 7bcd49c6efc8801b1b474c5a8ca5d93643b900c8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 7 Aug 2023 21:59:54 +0000 Subject: [PATCH 1/9] wip --- .../QuadraticForm/TensorProduct.lean | 130 ++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean new file mode 100644 index 00000000000000..5597c5847d9643 --- /dev/null +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2023 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eric Wieser +-/ +import Mathlib.LinearAlgebra.BilinearForm.TensorProduct +import Mathlib.LinearAlgebra.QuadraticForm.Basic + +/-! +# The quadratic form on a tensor product + +## Main definitions + +* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by applying + `B₁` on `M₁` and `B₂` on `M₂`. +* `QuadraticForm.tensorDistribEquiv`: `QuadraticForm.tensorDistrib` as an equivalence on finite free + modules. + +-/ + + +universe u v w uι uR uA uM₁ uM₂ + +variable {ι : Type _} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} + +open TensorProduct + +namespace QuadraticForm + +section CommSemiring +variable [CommSemiring R] [CommSemiring A] +variable [AddCommMonoid M₁] [AddCommMonoid M₂] +variable [Algebra R A] [Module R M₁] [Module A M₁] +variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] +variable [Module R M₂] [Invertible (2 : R)] + +instance : SMulCommClass R A (QuadraticForm A M₁) := QuadraticForm.smulComm + +instance : Module A (QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂) := + TensorProduct.leftModule +/-- 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 a larger ring than +the one on the right. -/ +def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := +_ ∘ₗ BilinForm.tensorDistrib ∘ₗ AlgebraTensorModule.map _ _ + + +#exit +-- 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₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) + (m₁' : M₁) (m₂' : M₂) : + tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₂ m₂ m₂' • B₁ m₁ m₁' := + rfl +#align bilin_form.tensor_distrib_tmul QuadraticForm.tensorDistrib_tmulₓ + +/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +@[reducible] +protected def tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) : QuadraticForm A (M₁ ⊗[R] M₂) := + tensorDistrib (A := A) (B₁ ⊗ₜ[R] B₂) +#align bilin_form.tmul QuadraticForm.tmul + +/-- The base change of a bilinear form. -/ +protected def baseChange (B : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := + QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B + +@[simp] +theorem baseChange_tmul (B₂ : QuadraticForm R M₂) (a : A) (m₂ : M₂) + (a' : A) (m₂' : M₂) : + B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := + rfl + +end CommSemiring + +section CommRing + +variable [CommRing R] + +variable [AddCommGroup M₁] [AddCommGroup M₂] + +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₂] + +variable [Nontrivial R] + +/-- `tensorDistrib` as an equivalence. -/ +noncomputable def tensorDistribEquiv : + QuadraticForm R M₁ ⊗[R] QuadraticForm R M₂ ≃ₗ[R] QuadraticForm R (M₁ ⊗[R] M₂) := + -- the same `LinearEquiv`s as from `tensorDistrib`, + -- but with the inner linear map also as an equiv + TensorProduct.congr (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) + (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) ≪≫ₗ + TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ + (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ + (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin +#align bilin_form.tensor_distrib_equiv QuadraticForm.tensorDistribEquiv + + +@[simp] +theorem tensorDistribEquiv_tmul (B₁ : QuadraticForm R M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) + (m₁' : M₁) (m₂' : M₂) : + tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₁ m₁ m₁' * B₂ m₂ m₂' := + rfl + +variable (R M₁ M₂) in +-- TODO: make this `rfl` +@[simp] +theorem tensorDistribEquiv_toLinearMap : + (tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib (A := R) := by + ext B₁ B₂ : 3 + apply toLin.injective + ext + exact mul_comm _ _ + +@[simp] +theorem tensorDistribEquiv_apply (B : QuadraticForm R M₁ ⊗ QuadraticForm R M₂) : + tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (A := R) B := + FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B +#align bilin_form.tensor_distrib_equiv_apply QuadraticForm.tensorDistribEquiv_apply + +end CommRing + +end QuadraticForm From b14cba2496274e37aa83df70d21b650219863eb4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 15:13:47 +0000 Subject: [PATCH 2/9] wip --- .../QuadraticForm/TensorProduct.lean | 97 +++++-------------- 1 file changed, 24 insertions(+), 73 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 5597c5847d9643..d0fc69bab291c3 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -11,8 +11,8 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic ## Main definitions -* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by applying - `B₁` on `M₁` and `B₂` on `M₂`. +* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the quadratic form on `M₁ ⊗ M₂` constructed by applying + `B₁` on `M₁` and `B₂` on `M₂`. This construction is not available in characteristic two. * `QuadraticForm.tensorDistribEquiv`: `QuadraticForm.tensorDistrib` as an equivalence on finite free modules. @@ -27,33 +27,37 @@ open TensorProduct namespace QuadraticForm -section CommSemiring -variable [CommSemiring R] [CommSemiring A] -variable [AddCommMonoid M₁] [AddCommMonoid M₂] +section CommRing +variable [CommRing R] [CommRing A] +variable [AddCommGroup M₁] [AddCommGroup M₂] variable [Algebra R A] [Module R M₁] [Module A M₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] variable [Module R M₂] [Invertible (2 : R)] -instance : SMulCommClass R A (QuadraticForm A M₁) := QuadraticForm.smulComm - instance : Module A (QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂) := TensorProduct.leftModule -/-- 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 a larger ring than + +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. -/ def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := -_ ∘ₗ BilinForm.tensorDistrib ∘ₗ AlgebraTensorModule.map _ _ + BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) + ∘ₗ BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + ∘ₗ AlgebraTensorModule.map + (QuadraticForm.associatedHom A : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticForm.associatedHom R : QuadraticForm R M₁ →ₗ[R] BilinForm R M₁) -#exit --- 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. +-- 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 (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = B₂ m₂ m₂' • B₁ m₁ m₁' := + tensorDistrib (A := A) (Q₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = Q₂ m₂ • Q₁ m₁ := rfl #align bilin_form.tensor_distrib_tmul QuadraticForm.tensorDistrib_tmulₓ @@ -64,67 +68,14 @@ protected def tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) : #align bilin_form.tmul QuadraticForm.tmul /-- The base change of a bilinear form. -/ -protected def baseChange (B : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := - QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B +protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := + QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq) Q @[simp] -theorem baseChange_tmul (B₂ : QuadraticForm R M₂) (a : A) (m₂ : M₂) - (a' : A) (m₂' : M₂) : - B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := +theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : + Q.baseChange (a ⊗ₜ m₂) = Q m₂ • a := rfl end CommSemiring -section CommRing - -variable [CommRing R] - -variable [AddCommGroup M₁] [AddCommGroup M₂] - -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₂] - -variable [Nontrivial R] - -/-- `tensorDistrib` as an equivalence. -/ -noncomputable def tensorDistribEquiv : - QuadraticForm R M₁ ⊗[R] QuadraticForm R M₂ ≃ₗ[R] QuadraticForm R (M₁ ⊗[R] M₂) := - -- the same `LinearEquiv`s as from `tensorDistrib`, - -- but with the inner linear map also as an equiv - TensorProduct.congr (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) - (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) ≪≫ₗ - TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ - (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ - (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin -#align bilin_form.tensor_distrib_equiv QuadraticForm.tensorDistribEquiv - - -@[simp] -theorem tensorDistribEquiv_tmul (B₁ : QuadraticForm R M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) - (m₁' : M₁) (m₂' : M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = B₁ m₁ m₁' * B₂ m₂ m₂' := - rfl - -variable (R M₁ M₂) in --- TODO: make this `rfl` -@[simp] -theorem tensorDistribEquiv_toLinearMap : - (tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib (A := R) := by - ext B₁ B₂ : 3 - apply toLin.injective - ext - exact mul_comm _ _ - -@[simp] -theorem tensorDistribEquiv_apply (B : QuadraticForm R M₁ ⊗ QuadraticForm R M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (A := R) B := - FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B -#align bilin_form.tensor_distrib_equiv_apply QuadraticForm.tensorDistribEquiv_apply - -end CommRing - end QuadraticForm From 4ad432b9abacf2804e0a90bd766bcbfa8fcd004c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 15:36:52 +0000 Subject: [PATCH 3/9] update --- .../QuadraticForm/TensorProduct.lean | 45 +++++++++---------- 1 file changed, 20 insertions(+), 25 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index d0fc69bab291c3..9997d2cb2fd74e 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -11,10 +11,8 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic ## Main definitions -* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the quadratic form on `M₁ ⊗ M₂` constructed by applying - `B₁` on `M₁` and `B₂` on `M₂`. This construction is not available in characteristic two. -* `QuadraticForm.tensorDistribEquiv`: `QuadraticForm.tensorDistrib` as an equivalence on finite free - modules. +* `QuadraticForm.tensorDistrib (Q₁ ⊗ₜ Q₂)`: the quadratic form on `M₁ ⊗ M₂` constructed by applying + `Q₁` on `M₁` and `Q₂` on `M₂`. This construction is not available in characteristic two. -/ @@ -34,9 +32,6 @@ variable [Algebra R A] [Module R M₁] [Module A M₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] variable [Module R M₂] [Invertible (2 : R)] -instance : Module A (QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂) := - TensorProduct.leftModule - variable (R A) in /-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. @@ -44,37 +39,37 @@ 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. -/ def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := - BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) - ∘ₗ BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) - ∘ₗ AlgebraTensorModule.map + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + let toQ := BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) + let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + let toB := AlgebraTensorModule.map (QuadraticForm.associatedHom A : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticForm.associatedHom R : QuadraticForm R M₁ →ₗ[R] BilinForm R M₁) - + (QuadraticForm.associatedHom R : 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₂`. @[simp] -theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) - (m₁' : M₁) (m₂' : M₂) : - tensorDistrib (A := A) (Q₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = Q₂ m₂ • Q₁ m₁ := - rfl -#align bilin_form.tensor_distrib_tmul QuadraticForm.tensorDistrib_tmulₓ - -/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +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 + (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. -/ @[reducible] -protected def tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) : QuadraticForm A (M₁ ⊗[R] M₂) := - tensorDistrib (A := A) (B₁ ⊗ₜ[R] B₂) -#align bilin_form.tmul QuadraticForm.tmul +protected def tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : + QuadraticForm A (M₁ ⊗[R] M₂) := + tensorDistrib (A := A) (Q₁ ⊗ₜ[R] Q₂) -/-- The base change of a bilinear form. -/ +/-- The base change of a quadratic form. -/ protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq) Q @[simp] theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : Q.baseChange (a ⊗ₜ m₂) = Q m₂ • a := - rfl + tensorDistrib_tmul _ _ end CommSemiring From 71a91116cab3bc963b134c7fa910d36b3e192538 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 16:32:59 +0000 Subject: [PATCH 4/9] cleanup --- .../QuadraticForm/TensorProduct.lean | 30 ++++++++++++------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 9997d2cb2fd74e..891cb0ed6e76d2 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -16,10 +16,9 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic -/ +universe uι uR uA uM₁ uM₂ -universe u v w uι uR uA uM₁ uM₂ - -variable {ι : Type _} {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₂} open TensorProduct @@ -57,20 +56,31 @@ theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ -@[reducible] -protected def tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : +protected abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm A (M₁ ⊗[R] M₂) := - tensorDistrib (A := A) (Q₁ ⊗ₜ[R] Q₂) + 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, BilinForm.tmul] + dsimp + convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) /-- The base change of a quadratic form. -/ protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := - QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq) Q + QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq (R := A)) Q @[simp] theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : - Q.baseChange (a ⊗ₜ m₂) = Q m₂ • a := - tensorDistrib_tmul _ _ + Q.baseChange (a ⊗ₜ m₂) = Q m₂ • (a * a) := + tensorDistrib_tmul _ _ _ _ + +@[simp] +theorem associated_baseChange (Q : QuadraticForm R M₂) : + associated (R₁ := A) Q.baseChange = (associated (R := R) Q).baseChange := + associated_tmul _ Q -end CommSemiring +end CommRing end QuadraticForm From 301236d1825bca5c06109b1e8515798a7f3381e7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 16:36:02 +0000 Subject: [PATCH 5/9] add import --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index ed74b98b7cce33..3eeffbe9c45016 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2259,6 +2259,7 @@ import Mathlib.LinearAlgebra.QuadraticForm.Complex import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv import Mathlib.LinearAlgebra.QuadraticForm.Prod import Mathlib.LinearAlgebra.QuadraticForm.Real +import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct import Mathlib.LinearAlgebra.Quotient import Mathlib.LinearAlgebra.QuotientPi import Mathlib.LinearAlgebra.Ray From 11339396f023100b4d4407efd6912d412d4736de Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 17:00:30 +0000 Subject: [PATCH 6/9] fix --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 891cb0ed6e76d2..8c3b2607d6f231 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -42,8 +42,8 @@ def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] Q let toQ := BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map - (QuadraticForm.associatedHom A : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticForm.associatedHom R : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) + (QuadraticForm.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticForm.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 @@ -77,8 +77,8 @@ theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : tensorDistrib_tmul _ _ _ _ @[simp] -theorem associated_baseChange (Q : QuadraticForm R M₂) : - associated (R₁ := A) Q.baseChange = (associated (R := R) Q).baseChange := +theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : + associated (R₁ := A) Q.baseChange = (associated (R₁ := R) Q).baseChange := associated_tmul _ Q end CommRing From 4f85ca3c3e961515a03e8785ec34faeb9463e3b2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 17:27:09 +0000 Subject: [PATCH 7/9] helper lemma --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 5 +++++ Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 10 ++++++---- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 74e3b800c58e5b..1e9b3dcac3f8ec 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -883,6 +883,11 @@ theorem associated_linMulLin (f g : M →ₗ[R₁] R₁) : ring #align quadratic_form.associated_lin_mul_lin QuadraticForm.associated_linMulLin +@[simp] +lemma associated_sq : associated (R₁ := R₁) sq = LinearMap.toBilin (LinearMap.mul R₁ R₁) := + (associated_linMulLin (LinearMap.id) (LinearMap.id)).trans <| + by simp only [smul_add, invOf_two_smul_add_invOf_two_smul]; rfl + end Associated section Anisotropic diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 8c3b2607d6f231..6fb2cf3223985c 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -67,19 +67,21 @@ theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ dsimp convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) +variable (A) in /-- The base change of a quadratic form. -/ protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq (R := A)) Q @[simp] theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : - Q.baseChange (a ⊗ₜ m₂) = Q m₂ • (a * a) := + Q.baseChange A (a ⊗ₜ m₂) = Q m₂ • (a * a) := tensorDistrib_tmul _ _ _ _ -@[simp] + theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : - associated (R₁ := A) Q.baseChange = (associated (R₁ := R) Q).baseChange := - associated_tmul _ Q + associated (R₁ := A) (Q.baseChange A) = (associated (R₁ := R) Q).baseChange A := by + dsimp only [QuadraticForm.baseChange, BilinForm.baseChange] + rw [associated_tmul (QuadraticForm.sq (R := A)) Q, associated_sq] end CommRing From 0e1ef110b99da72ddc93230f03494cd06d8d73a4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 18 Aug 2023 07:11:53 +0100 Subject: [PATCH 8/9] Update Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean Co-authored-by: Alex J Best --- 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 6fb2cf3223985c..3e35eb9fbbea8a 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -16,9 +16,9 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic -/ -universe uι uR uA uM₁ uM₂ +universe uR uA uM₁ uM₂ -variable {ι : Type uι} {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₂} open TensorProduct From 26ec19453aa3a66f3c1e4ef7864e2172fa999ab2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 11:49:11 +0100 Subject: [PATCH 9/9] Update Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 3e35eb9fbbea8a..ec9ca8c28c422a 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -39,6 +39,8 @@ Note this is heterobasic; the quadratic form on the left can take values in a la the one on the right. -/ 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 := BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map