diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 4bd5271071266b..71fd73cfcb637e 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -5,6 +5,7 @@ Authors: Eric Wieser -/ import Mathlib.LinearAlgebra.BilinearForm import Mathlib.LinearAlgebra.TensorProduct +import Mathlib.LinearAlgebra.TensorProduct.Tower #align_import linear_algebra.bilinear_form.tensor_product from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9" @@ -21,52 +22,76 @@ import Mathlib.LinearAlgebra.TensorProduct -/ -universe u v w +universe u v w uι uR uA uM₁ uM₂ -variable {ι : Type*} {R : Type*} {M₁ M₂ : Type*} +variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} open TensorProduct namespace BilinForm section CommSemiring - -variable [CommSemiring R] - +variable [CommSemiring R] [CommSemiring A] variable [AddCommMonoid M₁] [AddCommMonoid M₂] - -variable [Module R M₁] [Module R M₂] - -/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ -def tensorDistrib : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂) := - ((TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ - (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin).toLinearMap ∘ₗ - TensorProduct.dualDistrib R _ _ ∘ₗ - (TensorProduct.congr (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) +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₂] + +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 + ≪≫ₗ LinearMap.toBilin).toLinearMap + ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _ + ∘ₗ (TensorProduct.AlgebraTensorModule.congr + (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv A _ _ _) (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap #align bilin_form.tensor_distrib BilinForm.tensorDistrib +-- 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 R M₁) (B₂ : BilinForm R M₂) (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 := R) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := + tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₂ m₂ m₂' • B₁ m₁ m₁' := rfl -#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmul +#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ @[reducible] -protected def tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) : BilinForm R (M₁ ⊗[R] M₂) := - tensorDistrib (R := R) (B₁ ⊗ₜ[R] B₂) +protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) := + tensorDistrib R A (B₁ ⊗ₜ[R] B₂) #align bilin_form.tmul BilinForm.tmul attribute [ext] TensorProduct.ext in /-- A tensor product of symmetric bilinear forms is symmetric. -/ -lemma IsSymm.tmul {B₁ : BilinForm R M₁} {B₂ : BilinForm R M₂} +lemma IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by rw [isSymm_iff_flip R] apply toLin.injective ext x₁ x₂ y₁ y₂ - exact (congr_arg₂ (HMul.hMul) (hB₁ x₁ y₁) (hB₂ x₂ y₂)).symm + exact (congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)).symm + +variable (A) in +/-- The base change of a bilinear form. -/ +protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := + BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B + +@[simp] +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 + +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 @@ -84,6 +109,7 @@ variable [Module.Free R M₂] [Module.Finite R M₂] 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₂) := @@ -96,10 +122,28 @@ noncomputable def tensorDistribEquiv : (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin #align bilin_form.tensor_distrib_equiv BilinForm.tensorDistribEquiv +-- this is a dsimp lemma +@[simp, nolint simpNF] +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₂' := + rfl + +variable (R M₁ M₂) in +-- TODO: make this `rfl` +@[simp] +theorem tensorDistribEquiv_toLinearMap : + (tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib R R := by + ext B₁ B₂ : 3 + apply toLin.injective + ext + exact mul_comm _ _ + @[simp] theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (R := R) B := - rfl + tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B := + FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B #align bilin_form.tensor_distrib_equiv_apply BilinForm.tensorDistribEquiv_apply end CommRing diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index f90a2c1873657f..a17beaf3ee1bd4 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -8,6 +8,7 @@ import Mathlib.LinearAlgebra.Projection import Mathlib.LinearAlgebra.SesquilinearForm import Mathlib.RingTheory.Finiteness import Mathlib.LinearAlgebra.FreeModule.Finite.Basic +import Mathlib.RingTheory.TensorProduct #align_import linear_algebra.dual from "leanprover-community/mathlib"@"b1c017582e9f18d8494e5c18602a8cb4a6f843ac" @@ -96,9 +97,9 @@ noncomputable section namespace Module -- Porting note: max u v universe issues so name and specific below -universe u v v' v'' w u₁ u₂ +universe u uA v v' v'' w u₁ u₂ -variable (R : Type u) (M : Type v) +variable (R : Type u) (A : Type uA) (M : Type v) variable [CommSemiring R] [AddCommMonoid M] [Module R M] @@ -1566,7 +1567,7 @@ end VectorSpace namespace TensorProduct -variable (R : Type*) (M : Type*) (N : Type*) +variable (R A : Type*) (M : Type*) (N : Type*) variable {ι κ : Type*} @@ -1608,6 +1609,24 @@ theorem dualDistrib_apply (f : Dual R M) (g : Dual R N) (m : M) (n : N) : end +namespace AlgebraTensorModule +variable [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] + +variable [Module R M] [Module A M] [Module R N] [IsScalarTower R A M] + +/-- Heterobasic version of `TensorProduct.dualDistrib` -/ +def dualDistrib : Dual A M ⊗[R] Dual R N →ₗ[A] Dual A (M ⊗[R] N) := + compRight (Algebra.TensorProduct.rid R A A) ∘ₗ homTensorHomMap R A A M N A R + +variable {R M N} + +@[simp] +theorem dualDistrib_apply (f : Dual A M) (g : Dual R N) (m : M) (n : N) : + dualDistrib R A M N (f ⊗ₜ g) (m ⊗ₜ n) = g n • f m := + rfl + +end AlgebraTensorModule + variable {R M N} variable [CommRing R] [AddCommGroup M] [AddCommGroup N]