From e0a32a08ed83039484842a054d4e4d003ef3353c Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 1 Jan 2024 21:24:12 +0000 Subject: [PATCH 01/60] initial --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 206 ++++++++++++++++++++- 1 file changed, 204 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index d4781066bd33e2..7e65bd8bce2085 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -6,6 +6,7 @@ Authors: Frédéric Dupuis, Eric Wieser import Mathlib.GroupTheory.Congruence import Mathlib.LinearAlgebra.Multilinear.TensorProduct import Mathlib.Tactic.LibrarySearch +import Mathlib.Tactic.Ring.RingNF #align_import linear_algebra.pi_tensor_product from "leanprover-community/mathlib"@"ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a" @@ -530,7 +531,7 @@ variable (ι) attribute [local simp] eq_iff_true_of_subsingleton in /-- The tensor product over an empty index type `ι` is isomorphic to the base ring. -/ @[simps symm_apply] -def isEmptyEquiv [IsEmpty ι] : (⨂[R] _ : ι, M) ≃ₗ[R] R where +def isEmptyEquiv [IsEmpty ι] : (⨂[R] i : ι, s i) ≃ₗ[R] R where toFun := lift (constOfIsEmpty R _ 1) invFun r := r • tprod R (@isEmptyElim _ _ _) left_inv x := by @@ -551,7 +552,8 @@ def isEmptyEquiv [IsEmpty ι] : (⨂[R] _ : ι, M) ≃ₗ[R] R where #align pi_tensor_product.is_empty_equiv PiTensorProduct.isEmptyEquiv @[simp] -theorem isEmptyEquiv_apply_tprod [IsEmpty ι] (f : ι → M) : isEmptyEquiv ι (tprod R f) = 1 := +theorem isEmptyEquiv_apply_tprod [IsEmpty ι] (f : (i : ι) → s i) : + isEmptyEquiv ι (tprod R f) = 1 := lift.tprod _ #align pi_tensor_product.is_empty_equiv_apply_tprod PiTensorProduct.isEmptyEquiv_apply_tprod @@ -678,6 +680,206 @@ this is false in the case where `ι` is empty. -/ instance : AddCommGroup (⨂[R] i, s i) := Module.addCommMonoidToAddCommGroup R +section algebra + +variable {A : ι → Type*} [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] + +/-- +The multiplication in tensor product of rings is given by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` +-/ +def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := +lift +{ toFun := fun x ↦ lift + { toFun := fun y ↦ tprod _ (x * y) + map_add' := fun z i a a' ↦ by + dsimp + rw [show x * update z i (a + a') = update (x * z) i (x i * (a + a')) by + · ext j + simp only [Pi.mul_apply, update] + aesop] + rw [mul_add, MultilinearMap.map_add] + congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop + map_smul' := fun z i r a ↦ by + dsimp + rw [show x * update z i (r • a) = update (x * z) i (x i * (r • a)) by + · ext j + simp only [Pi.mul_apply, update, Algebra.mul_smul_comm] + split_ifs <;> aesop, + show x i * r • a = r • (x i * a) by + · rw [Algebra.smul_def, ← mul_assoc, mul_comm (x i), mul_assoc, Algebra.smul_def]] + rw [MultilinearMap.map_smul] + congr + ext j + simp only [update, Pi.mul_apply] + aesop } + map_add' := fun z i a a' ↦ by + ext z' + simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, + LinearMap.add_apply] + rw [show update z i (a + a') * z' = update (z * z') i ((a + a') * (z' i)) by + · ext j + simp only [Pi.mul_apply, update] + aesop] + rw [add_mul, MultilinearMap.map_add] + congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop + map_smul' := fun z i r a ↦ by + ext z' + simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, + LinearMap.smul_apply] + rw [show update z i (r • a) * z' = update (z * z') i ((r • a) * z' i) by + · ext j + simp only [Pi.mul_apply, update] + aesop] + rw [Algebra.smul_mul_assoc, MultilinearMap.map_smul] + congr + ext j + simp only [update, Pi.mul_apply] + aesop } + +@[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : + lmul (tprod R x) (tprod R y) = tprod R (x * y) := by + simp only [lmul, lift.tprod, MultilinearMap.coe_mk] + +set_option maxHeartbeats 500000 in +lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by + have reorder0 : ∀ (a b c d : ⨂[R] i, A i), a + b + (c + d) = (a + c) + (b + d) + · intros; abel + have reorder1 : + ∀ (a b c d e f g h : ⨂[R] i, A i), a + b + (c + d) + (e + f + (g + h)) = + (a + c + (e + g)) + (b + d + (f + h)) + · intros; abel + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ <;> + induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ <;> + induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ + · simp [mul_assoc] + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ + rw [hz₁, hz₂] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, + smul_add] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ hz₁ hz₂ ⊢ + rw [reorder0, hy₁, hy₂, ← add_assoc, ← add_assoc] + congr 1 + rw [add_assoc, add_assoc] + congr 1 + rw [add_comm] + · simp only [map_add, map_smul, LinearMap.add_apply, smul_add, LinearMap.smul_apply, + lmul_tprod_tprod] at hx₁ hx₂ ⊢ + rw [hx₁, hx₂] + · simp only [map_smul, map_add, LinearMap.smul_apply, LinearMap.add_apply, + smul_add] at hx₁ hx₂ hz₁ hz₂ ⊢ + rw [reorder0, hx₁, hx₂, ← add_assoc, ← add_assoc] + congr 1 + rw [add_assoc, add_assoc] + congr 1 + rw [add_comm] + · simp only [map_add, LinearMap.add_apply, map_smul, smul_add] at hx₁ hx₂ ⊢ + rw [reorder0, hx₁, hx₂, ← add_assoc, ← add_assoc] + congr 1 + rw [add_assoc, add_assoc] + congr 1 + rw [add_comm] + · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ + conv_lhs => rw [reorder1, hx₁, hx₂] + conv_rhs => rw [reorder1] + +lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · simp + · simp only [map_add, hx₁, hx₂] + +lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · simp + · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] + +lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by + have reorder0 : ∀ (a b c d : ⨂[R] i, A i), a + b + (c + d) = (a + c) + (b + d) + · intros; abel + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ <;> + induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] + rw [smul_comm, mul_comm] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, smul_add] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] + · simp [map_add, map_smul, LinearMap.add_apply, smul_add, LinearMap.smul_apply] at hx₁ hx₂ ⊢ + rw [hx₁, hx₂] + · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ + rw [reorder0, hx₁] + congr + +lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by + induction' x using PiTensorProduct.induction_on <;> simp + +lemma lmul_zero (x : ⨂[R] i, A i) : lmul x 0 = 0 := by + induction' x using PiTensorProduct.induction_on <;> simp + +lemma lmul_add (x y z : ⨂[R] i, A i) : lmul x (y + z) = lmul x y + lmul x z := by + induction' x using PiTensorProduct.induction_on <;> simp + +lemma add_lmul (x y z : ⨂[R] i, A i) : lmul (x + y) z = lmul x z + lmul y z := by + induction' x using PiTensorProduct.induction_on <;> simp + +instance mul : Mul (⨂[R] i, A i) where + mul x y := lmul x y + +lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl + +instance one : One (⨂[R] i, A i) where + one := tprod R 1 + +instance monoid : Monoid (⨂[R] i, A i) where + __ := mul + __ := one + mul_assoc := lmul_assoc + one_mul := one_lmul + mul_one := lmul_one + +instance commMonoid : CommMonoid (⨂[R] i, A i) where + __ := monoid + mul_comm := lmul_comm + +instance ring : Ring (⨂[R] i, A i) where + __ := commMonoid + __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) + left_distrib := lmul_add + right_distrib := add_lmul + zero_mul := zero_lmul + mul_zero := lmul_zero + +instance commRing : CommRing (⨂[R] i, A i) where + __ := commMonoid + __ := ring + +@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : + (tprod R x) * (tprod R y) = tprod R (x * y) := + lmul_tprod_tprod x y + +variable [DecidableEq ι] + +variable (R A) + +@[simps] +def fromComponentLinear (i : ι) : A i →ₗ[R] ⨂[R] i, A i where + toFun a := tprod R (Function.update 1 i a) + map_add' _ _ := MultilinearMap.map_add _ _ _ _ _ + map_smul' _ _ := MultilinearMap.map_smul _ _ _ _ _ + +@[simps] +def fromComponentRingHom (i : ι) : A i →+* ⨂[R] i, A i where + __ := fromComponentLinear R A i + map_one' := by aesop + map_mul' a b := by + simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, fromComponentLinear_apply, + tprod_mul_tprod] + congr + ext + simp only [update, Pi.one_apply, Pi.mul_apply] + aesop + map_zero' := by simp + +end algebra + end PiTensorProduct end Ring From 631bfe3f66ede357921741ac549ca62882a3995e Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 1 Jan 2024 23:31:00 +0000 Subject: [PATCH 02/60] Tensor product of algebra --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 89 ++++++++++++++++++---- 1 file changed, 73 insertions(+), 16 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 7e65bd8bce2085..61abfaf695b9c0 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -5,6 +5,7 @@ Authors: Frédéric Dupuis, Eric Wieser -/ import Mathlib.GroupTheory.Congruence import Mathlib.LinearAlgebra.Multilinear.TensorProduct +import Mathlib.Algebra.Algebra.Pi import Mathlib.Tactic.LibrarySearch import Mathlib.Tactic.Ring.RingNF @@ -680,6 +681,14 @@ this is false in the case where `ι` is empty. -/ instance : AddCommGroup (⨂[R] i, s i) := Module.addCommMonoidToAddCommGroup R +/-! +#### Tensor product of `R`-algebras + +If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor `⨂ᵢ Aᵢ` is an `R`-algebra as well with +its structure map defined by `r ↦ ⨂ rᵢ` where `rᵢ` is the image of `R` in `Aᵢ`. + +In particular if we take `R` to be `ℤ`, then this collapse into tensor product of rings. +-/ section algebra variable {A : ι → Type*} [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] @@ -855,28 +864,76 @@ instance commRing : CommRing (⨂[R] i, A i) where (tprod R x) * (tprod R y) = tprod R (x * y) := lmul_tprod_tprod x y -variable [DecidableEq ι] - -variable (R A) +lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : + (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by + change lmul _ _ = _ + rw [map_smul, map_smul, mul_comm r s, mul_smul] + simp only [LinearMap.smul_apply, lmul_tprod_tprod] + +instance algebra : Algebra R (⨂[R] i, A i) where + __ := hasSMul' + toFun := (· • 1) + map_one' := by simp + map_mul' r s :=show (r * s) • 1 = lmul (r • 1) (s • 1) by + rw [map_smul, map_smul, LinearMap.smul_apply, mul_comm, mul_smul] + congr + show (1 : ⨂[R] i, A i) = 1 * 1 + rw [mul_one] + map_zero' := by simp + map_add' := by simp [add_smul] + commutes' r x := by + simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] + change lmul _ _ = lmul _ _ + rw [map_smul, map_smul, LinearMap.smul_apply] + change r • (1 * x) = r • (x * 1) + rw [mul_comm] + smul_def' r x := by + simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] + change _ = lmul _ _ + rw [map_smul, LinearMap.smul_apply] + change _ = r • (1 * x) + rw [one_mul] +/-- +the map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` +-/ @[simps] -def fromComponentLinear (i : ι) : A i →ₗ[R] ⨂[R] i, A i where +def fromComponentAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where toFun a := tprod R (Function.update 1 i a) - map_add' _ _ := MultilinearMap.map_add _ _ _ _ _ - map_smul' _ _ := MultilinearMap.map_smul _ _ _ _ _ - -@[simps] -def fromComponentRingHom (i : ι) : A i →+* ⨂[R] i, A i where - __ := fromComponentLinear R A i - map_one' := by aesop - map_mul' a b := by - simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, fromComponentLinear_apply, - tprod_mul_tprod] + map_one' := by simp only [update_one]; rfl + map_mul' a a' := by + simp only [tprod_mul_tprod] congr - ext + ext j simp only [update, Pi.one_apply, Pi.mul_apply] aesop - map_zero' := by simp + map_zero' := MultilinearMap.map_update_zero _ _ _ + map_add' _ _ := MultilinearMap.map_add _ _ _ _ _ + commutes' r := show tprodCoeff R _ _ = r • tprodCoeff R _ _ by + rw [Algebra.algebraMap_eq_smul_one] + erw [smul_tprodCoeff] + rfl + +@[simps] +def liftAlgHom {S : Type*} [CommRing S] [Algebra R S] + (f : MultilinearMap R A S) + (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) : (⨂[R] i, A i) →ₐ[R] S where + toFun := lift f + map_one' := show lift f (tprod R 1) = 1 by simp [one] + map_mul' x y := show lift f (x * y) = lift f x * lift f y by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, tprod_mul_tprod, map_smul, + lift.tprod, mul] + · simp only [Algebra.smul_mul_assoc, map_smul, lift.tprod, map_add] at hy₁ hy₂ ⊢ + rw [mul_add, map_add, smul_add, hy₁, hy₂, mul_add, smul_add] + · simp only [map_add] at hx₁ hx₂ ⊢ + rw [add_mul, map_add, hx₁, hx₂, add_mul] + map_zero' := by simp only [map_zero] + map_add' x y := by simp only [map_add] + commutes' r := show lift f (r • tprod R 1) = _ by + rw [map_smul, lift.tprod, one, Algebra.algebraMap_eq_smul_one] end algebra From da25cda0a13b82e8542398f456ebf13b12713ee5 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 1 Jan 2024 23:41:46 +0000 Subject: [PATCH 03/60] better proof --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 69 ++++++---------------- 1 file changed, 17 insertions(+), 52 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 61abfaf695b9c0..28a19e38682df2 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -749,48 +749,17 @@ lift lmul (tprod R x) (tprod R y) = tprod R (x * y) := by simp only [lmul, lift.tprod, MultilinearMap.coe_mk] -set_option maxHeartbeats 500000 in lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by - have reorder0 : ∀ (a b c d : ⨂[R] i, A i), a + b + (c + d) = (a + c) + (b + d) - · intros; abel - have reorder1 : - ∀ (a b c d e f g h : ⨂[R] i, A i), a + b + (c + d) + (e + f + (g + h)) = - (a + c + (e + g)) + (b + d + (f + h)) - · intros; abel - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ <;> - induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ <;> - induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ - · simp [mul_assoc] - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ - rw [hz₁, hz₂] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, - smul_add] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ hz₁ hz₂ ⊢ - rw [reorder0, hy₁, hy₂, ← add_assoc, ← add_assoc] - congr 1 - rw [add_assoc, add_assoc] - congr 1 - rw [add_comm] - · simp only [map_add, map_smul, LinearMap.add_apply, smul_add, LinearMap.smul_apply, - lmul_tprod_tprod] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] - · simp only [map_smul, map_add, LinearMap.smul_apply, LinearMap.add_apply, - smul_add] at hx₁ hx₂ hz₁ hz₂ ⊢ - rw [reorder0, hx₁, hx₂, ← add_assoc, ← add_assoc] - congr 1 - rw [add_assoc, add_assoc] - congr 1 - rw [add_comm] - · simp only [map_add, LinearMap.add_apply, map_smul, smul_add] at hx₁ hx₂ ⊢ - rw [reorder0, hx₁, hx₂, ← add_assoc, ← add_assoc] - congr 1 - rw [add_assoc, add_assoc] - congr 1 - rw [add_comm] + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, mul_assoc] + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ + rw [hz₁, hz₂] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - conv_lhs => rw [reorder1, hx₁, hx₂] - conv_rhs => rw [reorder1] + rw [hx₁, hx₂] lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ @@ -803,19 +772,15 @@ lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by - have reorder0 : ∀ (a b c d : ⨂[R] i, A i), a + b + (c + d) = (a + c) + (b + d) - · intros; abel - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ <;> - induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] - rw [smul_comm, mul_comm] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, smul_add] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp [map_add, map_smul, LinearMap.add_apply, smul_add, LinearMap.smul_apply] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] + rw [smul_comm, mul_comm] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, + smul_add] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - rw [reorder0, hx₁] - congr + rw [hx₁, hx₂] lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by induction' x using PiTensorProduct.induction_on <;> simp From 345f1e69fc61d1f103ecd7b8cd662ca14047a16d Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 1 Jan 2024 23:42:40 +0000 Subject: [PATCH 04/60] unnecessary import --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 28a19e38682df2..9cd579fafdb66e 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -7,7 +7,6 @@ import Mathlib.GroupTheory.Congruence import Mathlib.LinearAlgebra.Multilinear.TensorProduct import Mathlib.Algebra.Algebra.Pi import Mathlib.Tactic.LibrarySearch -import Mathlib.Tactic.Ring.RingNF #align_import linear_algebra.pi_tensor_product from "leanprover-community/mathlib"@"ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a" From 65ec8810fa5a308ab8c477a007b6f3627fe3271f Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 2 Jan 2024 02:32:19 +0000 Subject: [PATCH 05/60] missing doc string --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 9cd579fafdb66e..10dd6f4d7b584e 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -878,6 +878,9 @@ def fromComponentAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i erw [smul_tprodCoeff] rfl +/-- +Lifting a multilinear map to an algebra homomorphism from tensor product +-/ @[simps] def liftAlgHom {S : Type*} [CommRing S] [Algebra R S] (f : MultilinearMap R A S) From de5d6d2e390a0bd6d072258b1ef3a387c079bb6c Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 3 Jan 2024 20:28:19 +0000 Subject: [PATCH 06/60] move file around --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 225 ------------------- Mathlib/RingTheory/PiTensorProduct.lean | 238 +++++++++++++++++++++ 2 files changed, 238 insertions(+), 225 deletions(-) create mode 100644 Mathlib/RingTheory/PiTensorProduct.lean diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 10dd6f4d7b584e..59f1c9cc2724df 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -5,7 +5,6 @@ Authors: Frédéric Dupuis, Eric Wieser -/ import Mathlib.GroupTheory.Congruence import Mathlib.LinearAlgebra.Multilinear.TensorProduct -import Mathlib.Algebra.Algebra.Pi import Mathlib.Tactic.LibrarySearch #align_import linear_algebra.pi_tensor_product from "leanprover-community/mathlib"@"ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a" @@ -680,230 +679,6 @@ this is false in the case where `ι` is empty. -/ instance : AddCommGroup (⨂[R] i, s i) := Module.addCommMonoidToAddCommGroup R -/-! -#### Tensor product of `R`-algebras - -If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor `⨂ᵢ Aᵢ` is an `R`-algebra as well with -its structure map defined by `r ↦ ⨂ rᵢ` where `rᵢ` is the image of `R` in `Aᵢ`. - -In particular if we take `R` to be `ℤ`, then this collapse into tensor product of rings. --/ -section algebra - -variable {A : ι → Type*} [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] - -/-- -The multiplication in tensor product of rings is given by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` --/ -def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := -lift -{ toFun := fun x ↦ lift - { toFun := fun y ↦ tprod _ (x * y) - map_add' := fun z i a a' ↦ by - dsimp - rw [show x * update z i (a + a') = update (x * z) i (x i * (a + a')) by - · ext j - simp only [Pi.mul_apply, update] - aesop] - rw [mul_add, MultilinearMap.map_add] - congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop - map_smul' := fun z i r a ↦ by - dsimp - rw [show x * update z i (r • a) = update (x * z) i (x i * (r • a)) by - · ext j - simp only [Pi.mul_apply, update, Algebra.mul_smul_comm] - split_ifs <;> aesop, - show x i * r • a = r • (x i * a) by - · rw [Algebra.smul_def, ← mul_assoc, mul_comm (x i), mul_assoc, Algebra.smul_def]] - rw [MultilinearMap.map_smul] - congr - ext j - simp only [update, Pi.mul_apply] - aesop } - map_add' := fun z i a a' ↦ by - ext z' - simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, - LinearMap.add_apply] - rw [show update z i (a + a') * z' = update (z * z') i ((a + a') * (z' i)) by - · ext j - simp only [Pi.mul_apply, update] - aesop] - rw [add_mul, MultilinearMap.map_add] - congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop - map_smul' := fun z i r a ↦ by - ext z' - simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, - LinearMap.smul_apply] - rw [show update z i (r • a) * z' = update (z * z') i ((r • a) * z' i) by - · ext j - simp only [Pi.mul_apply, update] - aesop] - rw [Algebra.smul_mul_assoc, MultilinearMap.map_smul] - congr - ext j - simp only [update, Pi.mul_apply] - aesop } - -@[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : - lmul (tprod R x) (tprod R y) = tprod R (x * y) := by - simp only [lmul, lift.tprod, MultilinearMap.coe_mk] - -lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, mul_assoc] - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ - rw [hz₁, hz₂] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] - -lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · simp - · simp only [map_add, hx₁, hx₂] - -lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · simp - · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] - -lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] - rw [smul_comm, mul_comm] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, - smul_add] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] - -lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by - induction' x using PiTensorProduct.induction_on <;> simp - -lemma lmul_zero (x : ⨂[R] i, A i) : lmul x 0 = 0 := by - induction' x using PiTensorProduct.induction_on <;> simp - -lemma lmul_add (x y z : ⨂[R] i, A i) : lmul x (y + z) = lmul x y + lmul x z := by - induction' x using PiTensorProduct.induction_on <;> simp - -lemma add_lmul (x y z : ⨂[R] i, A i) : lmul (x + y) z = lmul x z + lmul y z := by - induction' x using PiTensorProduct.induction_on <;> simp - -instance mul : Mul (⨂[R] i, A i) where - mul x y := lmul x y - -lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl - -instance one : One (⨂[R] i, A i) where - one := tprod R 1 - -instance monoid : Monoid (⨂[R] i, A i) where - __ := mul - __ := one - mul_assoc := lmul_assoc - one_mul := one_lmul - mul_one := lmul_one - -instance commMonoid : CommMonoid (⨂[R] i, A i) where - __ := monoid - mul_comm := lmul_comm - -instance ring : Ring (⨂[R] i, A i) where - __ := commMonoid - __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) - left_distrib := lmul_add - right_distrib := add_lmul - zero_mul := zero_lmul - mul_zero := lmul_zero - -instance commRing : CommRing (⨂[R] i, A i) where - __ := commMonoid - __ := ring - -@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : - (tprod R x) * (tprod R y) = tprod R (x * y) := - lmul_tprod_tprod x y - -lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : - (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by - change lmul _ _ = _ - rw [map_smul, map_smul, mul_comm r s, mul_smul] - simp only [LinearMap.smul_apply, lmul_tprod_tprod] - -instance algebra : Algebra R (⨂[R] i, A i) where - __ := hasSMul' - toFun := (· • 1) - map_one' := by simp - map_mul' r s :=show (r * s) • 1 = lmul (r • 1) (s • 1) by - rw [map_smul, map_smul, LinearMap.smul_apply, mul_comm, mul_smul] - congr - show (1 : ⨂[R] i, A i) = 1 * 1 - rw [mul_one] - map_zero' := by simp - map_add' := by simp [add_smul] - commutes' r x := by - simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] - change lmul _ _ = lmul _ _ - rw [map_smul, map_smul, LinearMap.smul_apply] - change r • (1 * x) = r • (x * 1) - rw [mul_comm] - smul_def' r x := by - simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] - change _ = lmul _ _ - rw [map_smul, LinearMap.smul_apply] - change _ = r • (1 * x) - rw [one_mul] - -/-- -the map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` --/ -@[simps] -def fromComponentAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where - toFun a := tprod R (Function.update 1 i a) - map_one' := by simp only [update_one]; rfl - map_mul' a a' := by - simp only [tprod_mul_tprod] - congr - ext j - simp only [update, Pi.one_apply, Pi.mul_apply] - aesop - map_zero' := MultilinearMap.map_update_zero _ _ _ - map_add' _ _ := MultilinearMap.map_add _ _ _ _ _ - commutes' r := show tprodCoeff R _ _ = r • tprodCoeff R _ _ by - rw [Algebra.algebraMap_eq_smul_one] - erw [smul_tprodCoeff] - rfl - -/-- -Lifting a multilinear map to an algebra homomorphism from tensor product --/ -@[simps] -def liftAlgHom {S : Type*} [CommRing S] [Algebra R S] - (f : MultilinearMap R A S) - (one : f 1 = 1) - (mul : ∀ x y, f (x * y) = f x * f y) : (⨂[R] i, A i) →ₐ[R] S where - toFun := lift f - map_one' := show lift f (tprod R 1) = 1 by simp [one] - map_mul' x y := show lift f (x * y) = lift f x * lift f y by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, tprod_mul_tprod, map_smul, - lift.tprod, mul] - · simp only [Algebra.smul_mul_assoc, map_smul, lift.tprod, map_add] at hy₁ hy₂ ⊢ - rw [mul_add, map_add, smul_add, hy₁, hy₂, mul_add, smul_add] - · simp only [map_add] at hx₁ hx₂ ⊢ - rw [add_mul, map_add, hx₁, hx₂, add_mul] - map_zero' := by simp only [map_zero] - map_add' x y := by simp only [map_add] - commutes' r := show lift f (r • tprod R 1) = _ by - rw [map_smul, lift.tprod, one, Algebra.algebraMap_eq_smul_one] - -end algebra - end PiTensorProduct end Ring diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean new file mode 100644 index 00000000000000..bd39b41e1da0a8 --- /dev/null +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -0,0 +1,238 @@ +/- +Copyright (c) 2024 Jujian Zhang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jujian Zhang +-/ + +import Mathlib.LinearAlgebra.PiTensorProduct +import Mathlib.Algebra.Algebra.Hom + +/-! +# Tensor product of `R`-algebras and rings + +If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor `⨂ᵢ Aᵢ` is an `R`-algebra as well with +its structure map defined by `r ↦ r • 1`. + +In particular if we take `R` to be `ℤ`, then this collapse into tensor product of rings. +-/ + +open TensorProduct Function + +noncomputable section + +namespace PiTensorProduct + +variable {ι R : Type*} {A : ι → Type*} [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] + +/-- +The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` +-/ +def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := +lift +{ toFun := fun x ↦ lift + { toFun := fun y ↦ tprod _ (x * y) + map_add' := fun z i a a' ↦ by + dsimp + rw [show x * update z i (a + a') = update (x * z) i (x i * (a + a')) by + · ext j + simp only [Pi.mul_apply, update] + aesop] + rw [mul_add, MultilinearMap.map_add] + congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop + map_smul' := fun z i r a ↦ by + dsimp + rw [show x * update z i (r • a) = update (x * z) i (x i * (r • a)) by + · ext j + simp only [Pi.mul_apply, update, Algebra.mul_smul_comm] + split_ifs <;> aesop, + show x i * r • a = r • (x i * a) by + · rw [Algebra.smul_def, ← mul_assoc, mul_comm (x i), mul_assoc, Algebra.smul_def]] + rw [MultilinearMap.map_smul] + congr + ext j + simp only [update, Pi.mul_apply] + aesop } + map_add' := fun z i a a' ↦ by + ext z' + simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, + LinearMap.add_apply] + rw [show update z i (a + a') * z' = update (z * z') i ((a + a') * (z' i)) by + · ext j + simp only [Pi.mul_apply, update] + aesop] + rw [add_mul, MultilinearMap.map_add] + congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop + map_smul' := fun z i r a ↦ by + ext z' + simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, + LinearMap.smul_apply] + rw [show update z i (r • a) * z' = update (z * z') i ((r • a) * z' i) by + · ext j + simp only [Pi.mul_apply, update] + aesop] + rw [Algebra.smul_mul_assoc, MultilinearMap.map_smul] + congr + ext j + simp only [update, Pi.mul_apply] + aesop } + +@[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : + lmul (tprod R x) (tprod R y) = tprod R (x * y) := by + simp only [lmul, lift.tprod, MultilinearMap.coe_mk] + +lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, mul_assoc] + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ + rw [hz₁, hz₂] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] + · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ + rw [hx₁, hx₂] + +lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · simp + · simp only [map_add, hx₁, hx₂] + +lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · simp + · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] + +lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] + rw [smul_comm, mul_comm] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, + smul_add] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] + · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ + rw [hx₁, hx₂] + +lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by + induction' x using PiTensorProduct.induction_on <;> simp + +lemma lmul_zero (x : ⨂[R] i, A i) : lmul x 0 = 0 := by + induction' x using PiTensorProduct.induction_on <;> simp + +lemma lmul_add (x y z : ⨂[R] i, A i) : lmul x (y + z) = lmul x y + lmul x z := by + induction' x using PiTensorProduct.induction_on <;> simp + +lemma add_lmul (x y z : ⨂[R] i, A i) : lmul (x + y) z = lmul x z + lmul y z := by + induction' x using PiTensorProduct.induction_on <;> simp + +instance mul : Mul (⨂[R] i, A i) where + mul x y := lmul x y + +lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl + +instance one : One (⨂[R] i, A i) where + one := tprod R 1 + +instance monoid : Monoid (⨂[R] i, A i) where + __ := mul + __ := one + mul_assoc := lmul_assoc + one_mul := one_lmul + mul_one := lmul_one + +instance commMonoid : CommMonoid (⨂[R] i, A i) where + __ := monoid + mul_comm := lmul_comm + +instance ring : Ring (⨂[R] i, A i) where + __ := commMonoid + __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) + left_distrib := lmul_add + right_distrib := add_lmul + zero_mul := zero_lmul + mul_zero := lmul_zero + +instance commRing : CommRing (⨂[R] i, A i) where + __ := commMonoid + __ := ring + +@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : + (tprod R x) * (tprod R y) = tprod R (x * y) := + lmul_tprod_tprod x y + +lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : + (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by + change lmul _ _ = _ + rw [map_smul, map_smul, mul_comm r s, mul_smul] + simp only [LinearMap.smul_apply, lmul_tprod_tprod] + +instance algebra : Algebra R (⨂[R] i, A i) where + __ := hasSMul' + toFun := (· • 1) + map_one' := by simp + map_mul' r s :=show (r * s) • 1 = lmul (r • 1) (s • 1) by + rw [map_smul, map_smul, LinearMap.smul_apply, mul_comm, mul_smul] + congr + show (1 : ⨂[R] i, A i) = 1 * 1 + rw [mul_one] + map_zero' := by simp + map_add' := by simp [add_smul] + commutes' r x := by + simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] + change lmul _ _ = lmul _ _ + rw [map_smul, map_smul, LinearMap.smul_apply] + change r • (1 * x) = r • (x * 1) + rw [mul_comm] + smul_def' r x := by + simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] + change _ = lmul _ _ + rw [map_smul, LinearMap.smul_apply] + change _ = r • (1 * x) + rw [one_mul] + +/-- +the map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` +-/ +@[simps] +def fromComponentAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where + toFun a := tprod R (Function.update 1 i a) + map_one' := by simp only [update_one]; rfl + map_mul' a a' := by + simp only [tprod_mul_tprod] + congr + ext j + simp only [update, Pi.one_apply, Pi.mul_apply] + aesop + map_zero' := MultilinearMap.map_update_zero _ _ _ + map_add' _ _ := MultilinearMap.map_add _ _ _ _ _ + commutes' r := show tprodCoeff R _ _ = r • tprodCoeff R _ _ by + rw [Algebra.algebraMap_eq_smul_one] + erw [smul_tprodCoeff] + rfl + +/-- +Lifting a multilinear map to an algebra homomorphism from tensor product +-/ +@[simps] +def liftAlgHom {S : Type*} [Semiring S] [Algebra R S] + (f : MultilinearMap R A S) + (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : (⨂[R] i, A i) →ₐ[R] S where + toFun := lift f + map_one' := show lift f (tprod R 1) = 1 by simp [one] + map_mul' x y := show lift f (x * y) = lift f x * lift f y by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, tprod_mul_tprod, map_smul, + lift.tprod, mul] + · simp only [Algebra.smul_mul_assoc, map_smul, lift.tprod, map_add] at hy₁ hy₂ ⊢ + rw [mul_add, map_add, smul_add, hy₁, hy₂, mul_add, smul_add] + · simp only [map_add] at hx₁ hx₂ ⊢ + rw [add_mul, map_add, hx₁, hx₂, add_mul] + map_zero' := by simp only [map_zero] + map_add' x y := by simp only [map_add] + commutes' r := show lift f (r • tprod R 1) = _ by + rw [map_smul, lift.tprod, one, Algebra.algebraMap_eq_smul_one] + +end PiTensorProduct + +end From d2261f441819aaa931e9090b5733512acdcdb850 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 3 Jan 2024 20:28:51 +0000 Subject: [PATCH 07/60] all import --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 2f1f1b2e3b072f..9ae7ffa936d628 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3145,6 +3145,7 @@ import Mathlib.RingTheory.Nullstellensatz import Mathlib.RingTheory.OreLocalization.Basic import Mathlib.RingTheory.OreLocalization.OreSet import Mathlib.RingTheory.Perfection +import Mathlib.RingTheory.PiTensorProduct import Mathlib.RingTheory.Polynomial.Basic import Mathlib.RingTheory.Polynomial.Bernstein import Mathlib.RingTheory.Polynomial.Chebyshev From 82d33c531b1d64e0dc1b5f5fe1c091f020419c20 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 3 Jan 2024 21:10:36 +0000 Subject: [PATCH 08/60] make `reindex` dependent --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 91 ++++++++++++---------- 1 file changed, 52 insertions(+), 39 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 59f1c9cc2724df..aeb6ff35d188c5 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -444,61 +444,58 @@ section variable (R M) -/-- Re-index the components of the tensor power by `e`. - -For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components. --/ -def reindex (e : ι ≃ ι₂) : (⨂[R] _ : ι, M) ≃ₗ[R] ⨂[R] _ : ι₂, M := - LinearEquiv.ofLinear (lift (domDomCongr e.symm (tprod R : MultilinearMap R _ (⨂[R] _ : ι₂, M)))) - (lift (domDomCongr e (tprod R : MultilinearMap R _ (⨂[R] _ : ι, M)))) - (by - ext - simp only [LinearMap.comp_apply, LinearMap.id_apply, lift_tprod, - LinearMap.compMultilinearMap_apply, lift.tprod, domDomCongr_apply] - congr - ext - rw [e.apply_symm_apply]) - (by - ext - simp only [LinearMap.comp_apply, LinearMap.id_apply, lift_tprod, - LinearMap.compMultilinearMap_apply, lift.tprod, domDomCongr_apply] - congr - ext - rw [e.symm_apply_apply]) +variable (s) in +/-- Re-index the components of the tensor power by `e`.-/ +def reindex (e : ι ≃ ι₂) : (⨂[R] i : ι, s i) ≃ₗ[R] ⨂[R] i : ι₂, s (e.symm i) := + let f := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s (e.symm i)) e + let g := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι), s i) e + LinearEquiv.ofLinear (lift <| f.symm <| tprod R) (lift <| g <| tprod R) (by aesop) (by aesop) #align pi_tensor_product.reindex PiTensorProduct.reindex end @[simp] -theorem reindex_tprod (e : ι ≃ ι₂) (f : ∀ _, M) : - reindex R M e (tprod R f) = tprod R fun i ↦ f (e.symm i) := by +theorem reindex_tprod (e : ι ≃ ι₂) (f : ∀ i, s i) : + reindex R s e (tprod R f) = tprod R fun i ↦ f (e.symm i) := by dsimp [reindex] exact liftAux_tprod _ f #align pi_tensor_product.reindex_tprod PiTensorProduct.reindex_tprod @[simp] theorem reindex_comp_tprod (e : ι ≃ ι₂) : - (reindex R M e : (⨂[R] _ : ι, M) →ₗ[R] ⨂[R] _ : ι₂, M).compMultilinearMap (tprod R) = - (tprod R : MultilinearMap R (fun _ ↦ M) _).domDomCongr e.symm := + (reindex R s e : (⨂[R] i : ι, s i) →ₗ[R] ⨂[R] i : ι₂, s (e.symm i)).compMultilinearMap + (tprod R) = + (domDomCongrLinearEquiv' R R s _ e).symm (tprod R) := MultilinearMap.ext <| reindex_tprod e #align pi_tensor_product.reindex_comp_tprod PiTensorProduct.reindex_comp_tprod @[simp] -theorem lift_comp_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun _ : ι₂ ↦ M) E) : - lift φ ∘ₗ ↑(reindex R M e) = lift (φ.domDomCongr e.symm) := by - ext - simp +theorem lift_comp_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i ↦ s (e.symm i)) E) : + lift φ ∘ₗ (reindex R s e) = lift ((domDomCongrLinearEquiv' R R s _ e).symm φ) := by + ext; simp [reindex] #align pi_tensor_product.lift_comp_reindex PiTensorProduct.lift_comp_reindex @[simp] -theorem lift_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun _ ↦ M) E) (x : ⨂[R] _, M) : - lift φ (reindex R M e x) = lift (φ.domDomCongr e.symm) x := +theorem lift_comp_reindex_symm (e : ι ≃ ι₂) (φ : MultilinearMap R s E) : + lift φ ∘ₗ (reindex R s e).symm = lift (domDomCongrLinearEquiv' R R s _ e φ) := by + ext; simp [reindex] + +@[simp] +theorem lift_reindex + (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i ↦ s (e.symm i)) E) (x : ⨂[R] i, s i) : + lift φ (reindex R s e x) = lift ((domDomCongrLinearEquiv' R R s _ e).symm φ) x := LinearMap.congr_fun (lift_comp_reindex e φ) x #align pi_tensor_product.lift_reindex PiTensorProduct.lift_reindex +@[simp] +theorem lift_reindex_symm + (e : ι ≃ ι₂) (φ : MultilinearMap R s E) (x : ⨂[R] i, s (e.symm i)) : + lift φ (reindex R s e |>.symm x) = lift (domDomCongrLinearEquiv' R R s _ e φ) x := + LinearMap.congr_fun (lift_comp_reindex_symm e φ) x + @[simp] theorem reindex_trans (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) : - (reindex R M e).trans (reindex R M e') = reindex R M (e.trans e') := by + (reindex R s e).trans (reindex R _ e') = reindex R s (e.trans e') := by apply LinearEquiv.toLinearMap_injective ext f simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod, @@ -508,21 +505,37 @@ theorem reindex_trans (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) : #align pi_tensor_product.reindex_trans PiTensorProduct.reindex_trans @[simp] -theorem reindex_reindex (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) (x : ⨂[R] _, M) : - reindex R M e' (reindex R M e x) = reindex R M (e.trans e') x := - LinearEquiv.congr_fun (reindex_trans e e' : _ = reindex R M (e.trans e')) x +theorem reindex_reindex (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) (x : ⨂[R] i, s i) : + reindex R _ e' (reindex R s e x) = reindex R s (e.trans e') x := + LinearEquiv.congr_fun (reindex_trans e e' : _ = reindex R s (e.trans e')) x #align pi_tensor_product.reindex_reindex PiTensorProduct.reindex_reindex +-- This doesn't have a dependent counterpart @[simp] -theorem reindex_symm (e : ι ≃ ι₂) : (reindex R M e).symm = reindex R M e.symm := rfl +theorem reindex_symm (e : ι ≃ ι₂) : + (reindex R (fun i ↦ M) e).symm = reindex R (fun i ↦ M) e.symm := by + ext x + simp only [reindex, domDomCongrLinearEquiv', LinearEquiv.coe_symm_mk, LinearEquiv.coe_mk, + LinearEquiv.ofLinear_symm_apply, Equiv.symm_symm_apply, LinearEquiv.ofLinear_apply] + refine x.induction_on ?_ ?_ + · intro r x + simp only [map_smul, lift.tprod, coe_mk, comp_apply, Equiv.symm_symm_apply] + congr + ext y j + simp + · intro x y hx hy + rw [map_add, map_add, hx, hy] #align pi_tensor_product.reindex_symm PiTensorProduct.reindex_symm @[simp] -theorem reindex_refl : reindex R M (Equiv.refl ι) = LinearEquiv.refl R _ := by +theorem reindex_refl : reindex R s (Equiv.refl ι) = LinearEquiv.refl R _ := by apply LinearEquiv.toLinearMap_injective ext - rw [reindex_comp_tprod, LinearEquiv.refl_toLinearMap, Equiv.refl_symm] - rfl + simp only [Equiv.refl_symm, Equiv.refl_apply, reindex, domDomCongrLinearEquiv', + LinearEquiv.coe_symm_mk, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, + LinearEquiv.refl_toLinearMap, LinearMap.id_coe, id_eq] + erw [lift.tprod] + congr #align pi_tensor_product.reindex_refl PiTensorProduct.reindex_refl variable (ι) From ad8b7f80894a60d2cdde6bdae1e7f09063b81c3d Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 3 Jan 2024 23:32:28 +0000 Subject: [PATCH 09/60] restructure --- Mathlib/RingTheory/PiTensorProduct.lean | 104 +++++++++++++++--------- 1 file changed, 64 insertions(+), 40 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index bd39b41e1da0a8..772632f547dc94 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -18,11 +18,26 @@ In particular if we take `R` to be `ℤ`, then this collapse into tensor product open TensorProduct Function -noncomputable section +variable {ι R : Type*} {A : ι → Type*} namespace PiTensorProduct -variable {ι R : Type*} {A : ι → Type*} [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] +noncomputable section AddCommMonoidWithOne + +variable [CommSemiring R] [∀ i, AddCommMonoidWithOne (A i)] [∀ i, Module R (A i)] + +instance one : One (⨂[R] i, A i) where + one := tprod R 1 + +instance addCommMonoidWithOne : AddCommMonoidWithOne (⨂[R] i, A i) where + __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i)) + __ := one + +end AddCommMonoidWithOne + +noncomputable section Semiring + +variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] /-- The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` @@ -45,8 +60,7 @@ lift · ext j simp only [Pi.mul_apply, update, Algebra.mul_smul_comm] split_ifs <;> aesop, - show x i * r • a = r • (x i * a) by - · rw [Algebra.smul_def, ← mul_assoc, mul_comm (x i), mul_assoc, Algebra.smul_def]] + show x i * r • a = r • (x i * a) by simp only [Algebra.mul_smul_comm]] rw [MultilinearMap.map_smul] congr ext j @@ -102,17 +116,6 @@ lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by · simp · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] -lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] - rw [smul_comm, mul_comm] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, - smul_add] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] - lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by induction' x using PiTensorProduct.induction_on <;> simp @@ -130,8 +133,15 @@ instance mul : Mul (⨂[R] i, A i) where lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl -instance one : One (⨂[R] i, A i) where - one := tprod R 1 +@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : + (tprod R x) * (tprod R y) = tprod R (x * y) := + lmul_tprod_tprod x y + +lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : + (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by + change lmul _ _ = _ + rw [map_smul, map_smul, mul_comm r s, mul_smul] + simp only [LinearMap.smul_apply, lmul_tprod_tprod] instance monoid : Monoid (⨂[R] i, A i) where __ := mul @@ -140,32 +150,14 @@ instance monoid : Monoid (⨂[R] i, A i) where one_mul := one_lmul mul_one := lmul_one -instance commMonoid : CommMonoid (⨂[R] i, A i) where +instance semiring : Semiring (⨂[R] i, A i) where __ := monoid - mul_comm := lmul_comm - -instance ring : Ring (⨂[R] i, A i) where - __ := commMonoid - __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) + __ := inferInstanceAs <| AddCommMonoid (⨂[R] i, A i) left_distrib := lmul_add right_distrib := add_lmul zero_mul := zero_lmul mul_zero := lmul_zero -instance commRing : CommRing (⨂[R] i, A i) where - __ := commMonoid - __ := ring - -@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : - (tprod R x) * (tprod R y) = tprod R (x * y) := - lmul_tprod_tprod x y - -lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : - (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by - change lmul _ _ = _ - rw [map_smul, map_smul, mul_comm r s, mul_smul] - simp only [LinearMap.smul_apply, lmul_tprod_tprod] - instance algebra : Algebra R (⨂[R] i, A i) where __ := hasSMul' toFun := (· • 1) @@ -182,7 +174,7 @@ instance algebra : Algebra R (⨂[R] i, A i) where change lmul _ _ = lmul _ _ rw [map_smul, map_smul, LinearMap.smul_apply] change r • (1 * x) = r • (x * 1) - rw [mul_comm] + rw [mul_one, one_mul] smul_def' r x := by simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] change _ = lmul _ _ @@ -233,6 +225,38 @@ def liftAlgHom {S : Type*} [Semiring S] [Algebra R S] commutes' r := show lift f (r • tprod R 1) = _ by rw [map_smul, lift.tprod, one, Algebra.algebraMap_eq_smul_one] -end PiTensorProduct +end Semiring + +noncomputable section Ring + +variable [CommRing R] [∀ i, Ring (A i)] [∀ i, Algebra R (A i)] + +instance ring : Ring (⨂[R] i, A i) where + __ := semiring + __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) + +end Ring + +noncomputable section CommRing + +variable [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] -end +lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] + rw [smul_comm, mul_comm] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, + smul_add] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] + · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ + rw [hx₁, hx₂] + +instance commRing : CommRing (⨂[R] i, A i) where + __ := ring + __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) + mul_comm := lmul_comm + +end CommRing + +end PiTensorProduct From 3f79bbd2cbcbacac5411eea2d620b198c7dd3c03 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 3 Jan 2024 23:40:41 +0000 Subject: [PATCH 10/60] fix --- Mathlib/LinearAlgebra/TensorPower.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean index b742de299280fa..75583ddc95783d 100644 --- a/Mathlib/LinearAlgebra/TensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorPower.lean @@ -52,8 +52,8 @@ are equal after a canonical reindexing. -/ @[ext] theorem gradedMonoid_eq_of_reindex_cast {ιι : Type*} {ι : ιι → Type*} : ∀ {a b : GradedMonoid fun ii => ⨂[R] _ : ι ii, M} (h : a.fst = b.fst), - reindex R M (Equiv.cast <| congr_arg ι h) a.snd = b.snd → a = b - | ⟨ai, a⟩, ⟨bi, b⟩ => fun (hi : ai = bi) (h : reindex R M _ a = b) => by + reindex R (fun _ ↦ M) (Equiv.cast <| congr_arg ι h) a.snd = b.snd → a = b + | ⟨ai, a⟩, ⟨bi, b⟩ => fun (hi : ai = bi) (h : reindex R (fun _ ↦ M) _ a = b) => by subst hi simp_all #align pi_tensor_product.graded_monoid_eq_of_reindex_cast PiTensorProduct.gradedMonoid_eq_of_reindex_cast @@ -78,7 +78,7 @@ theorem gOne_def : ₜ1 = tprod R (@Fin.elim0' M) := /-- A variant of `PiTensorProduct.tmulEquiv` with the result indexed by `Fin (n + m)`. -/ def mulEquiv {n m : ℕ} : (⨂[R]^n) M ⊗[R] (⨂[R]^m) M ≃ₗ[R] (⨂[R]^(n + m)) M := - (tmulEquiv R M).trans (reindex R M finSumFinEquiv) + (tmulEquiv R M).trans (reindex R (fun _ ↦ M) finSumFinEquiv) #align tensor_power.mul_equiv TensorPower.mulEquiv /-- As a graded monoid, `⨂[R]^i M` has a `(*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M`. -/ @@ -104,7 +104,7 @@ variable (R M) /-- Cast between "equal" tensor powers. -/ def cast {i j} (h : i = j) : (⨂[R]^i) M ≃ₗ[R] (⨂[R]^j) M := - reindex R M (Fin.castIso h).toEquiv + reindex R (fun _ ↦ M) (Fin.castIso h).toEquiv #align tensor_power.cast TensorPower.cast theorem cast_tprod {i j} (h : i = j) (a : Fin i → M) : @@ -114,7 +114,7 @@ theorem cast_tprod {i j} (h : i = j) (a : Fin i → M) : @[simp] theorem cast_refl {i} (h : i = i) : cast R M h = LinearEquiv.refl _ _ := - ((congr_arg fun f => reindex R M (RelIso.toEquiv f)) <| Fin.castIso_refl h).trans reindex_refl + ((congr_arg fun f => reindex R (fun _ ↦ M) (RelIso.toEquiv f)) <| Fin.castIso_refl h).trans reindex_refl #align tensor_power.cast_refl TensorPower.cast_refl @[simp] From 8a91d9b4d92b8a235b894e941aaca90533e05ea1 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 3 Jan 2024 23:41:58 +0000 Subject: [PATCH 11/60] long line --- Mathlib/LinearAlgebra/TensorPower.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean index 75583ddc95783d..a40c46ac1f5851 100644 --- a/Mathlib/LinearAlgebra/TensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorPower.lean @@ -114,7 +114,8 @@ theorem cast_tprod {i j} (h : i = j) (a : Fin i → M) : @[simp] theorem cast_refl {i} (h : i = i) : cast R M h = LinearEquiv.refl _ _ := - ((congr_arg fun f => reindex R (fun _ ↦ M) (RelIso.toEquiv f)) <| Fin.castIso_refl h).trans reindex_refl + ((congr_arg fun f => reindex R (fun _ ↦ M) (RelIso.toEquiv f)) <| Fin.castIso_refl h).trans + reindex_refl #align tensor_power.cast_refl TensorPower.cast_refl @[simp] From d56485bb14ba729f38c04e8b1502d5665090437a Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 3 Jan 2024 23:45:25 +0000 Subject: [PATCH 12/60] fix --- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean index 7cb1fcbf8a33e9..21ea4f375cf15c 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean @@ -120,7 +120,7 @@ theorem ofDirectSum_toDirectSum (x : TensorAlgebra R M) : @[simp, nolint simpNF] -- see std4#365 for the simpNF issue theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m - (PiTensorProduct.reindex R M (Equiv.cast <| congr_arg Fin h) x) = + (PiTensorProduct.reindex R (fun _ ↦ M) (Equiv.cast <| congr_arg Fin h) x) = GradedMonoid.mk n x := Eq.symm (PiTensorProduct.gradedMonoid_eq_of_reindex_cast h rfl) #align tensor_algebra.mk_reindex_cast TensorAlgebra.mk_reindex_cast @@ -128,7 +128,7 @@ theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : @[simp] theorem mk_reindex_fin_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m - (PiTensorProduct.reindex R M (Fin.castIso h).toEquiv x) = GradedMonoid.mk n x := by + (PiTensorProduct.reindex R (fun _ ↦ M) (Fin.castIso h).toEquiv x) = GradedMonoid.mk n x := by rw [Fin.castIso_to_equiv, mk_reindex_cast h] #align tensor_algebra.mk_reindex_fin_cast TensorAlgebra.mk_reindex_fin_cast From d0ab3a8fa755d5537f6e48fb25debd9006e624cb Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Thu, 4 Jan 2024 17:41:43 +0000 Subject: [PATCH 13/60] Update Mathlib/RingTheory/PiTensorProduct.lean Co-authored-by: Eric Wieser --- Mathlib/RingTheory/PiTensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 772632f547dc94..9b0fbe7fc1ae03 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -152,7 +152,7 @@ instance monoid : Monoid (⨂[R] i, A i) where instance semiring : Semiring (⨂[R] i, A i) where __ := monoid - __ := inferInstanceAs <| AddCommMonoid (⨂[R] i, A i) + __ := inferInstanceAs <| AddCommMonoidWithOne (⨂[R] i, A i) left_distrib := lmul_add right_distrib := add_lmul zero_mul := zero_lmul From a7e5617e4591a66a3fee10dfbf2a591f778ae741 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Thu, 4 Jan 2024 18:01:33 +0000 Subject: [PATCH 14/60] add commsemiring section --- Mathlib/RingTheory/PiTensorProduct.lean | 29 +++++++++++++++---------- 1 file changed, 17 insertions(+), 12 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 9b0fbe7fc1ae03..cb1ac4718a0213 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -6,6 +6,7 @@ Authors: Jujian Zhang import Mathlib.LinearAlgebra.PiTensorProduct import Mathlib.Algebra.Algebra.Hom +import Mathlib.Algebra.Group.Pi /-! # Tensor product of `R`-algebras and rings @@ -187,14 +188,9 @@ the map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` -/ @[simps] def fromComponentAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where - toFun a := tprod R (Function.update 1 i a) - map_one' := by simp only [update_one]; rfl - map_mul' a a' := by - simp only [tprod_mul_tprod] - congr - ext j - simp only [update, Pi.one_apply, Pi.mul_apply] - aesop + toFun a := tprod R (MonoidHom.single _ i a) + map_one' := by simp only [_root_.map_one]; rfl + map_mul' a a' := by simp map_zero' := MultilinearMap.map_update_zero _ _ _ map_add' _ _ := MultilinearMap.map_add _ _ _ _ _ commutes' r := show tprodCoeff R _ _ = r • tprodCoeff R _ _ by @@ -237,9 +233,9 @@ instance ring : Ring (⨂[R] i, A i) where end Ring -noncomputable section CommRing +noncomputable section CommSemiring -variable [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] +variable [CommSemiring R] [∀ i, CommSemiring (A i)] [∀ i, Algebra R (A i)] lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ @@ -252,10 +248,19 @@ lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ rw [hx₁, hx₂] +instance commSemiring : CommSemiring (⨂[R] i, A i) where + __ := semiring + __ := inferInstanceAs <| AddCommMonoid (⨂[R] i, A i) + mul_comm := lmul_comm + +end CommSemiring + +noncomputable section CommRing + +variable [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] instance commRing : CommRing (⨂[R] i, A i) where - __ := ring + __ := commSemiring __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) - mul_comm := lmul_comm end CommRing From a45e347021b59b8a47332b1c8a48873314285d7e Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Thu, 4 Jan 2024 18:21:40 +0000 Subject: [PATCH 15/60] nonAssocNonUnitalRing etc --- Mathlib/RingTheory/PiTensorProduct.lean | 122 +++++++++++++++--------- 1 file changed, 75 insertions(+), 47 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index cb1ac4718a0213..a5299c01e1da8e 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -36,9 +36,10 @@ instance addCommMonoidWithOne : AddCommMonoidWithOne (⨂[R] i, A i) where end AddCommMonoidWithOne -noncomputable section Semiring +noncomputable section NonUnitalNonAssocSemiring -variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] +variable [CommSemiring R] [∀ i, NonUnitalNonAssocSemiring (A i)] +variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] /-- The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` @@ -57,11 +58,12 @@ lift congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop map_smul' := fun z i r a ↦ by dsimp - rw [show x * update z i (r • a) = update (x * z) i (x i * (r • a)) by + rw [show x * update z i (r • a) = update (x * z) i (r • (x i * a)) by · ext j - simp only [Pi.mul_apply, update, Algebra.mul_smul_comm] - split_ifs <;> aesop, - show x i * r • a = r • (x i * a) by simp only [Algebra.mul_smul_comm]] + simp only [Pi.mul_apply, update, mul_smul_comm] + split_ifs with h + · subst h; simp only; rw [mul_smul_comm] + · aesop] rw [MultilinearMap.map_smul] congr ext j @@ -85,7 +87,7 @@ lift · ext j simp only [Pi.mul_apply, update] aesop] - rw [Algebra.smul_mul_assoc, MultilinearMap.map_smul] + rw [smul_mul_assoc, MultilinearMap.map_smul] congr ext j simp only [update, Pi.mul_apply] @@ -95,27 +97,20 @@ lift lmul (tprod R x) (tprod R y) = tprod R (x * y) := by simp only [lmul, lift.tprod, MultilinearMap.coe_mk] -lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, mul_assoc] - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ - rw [hz₁, hz₂] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] +instance mul : Mul (⨂[R] i, A i) where + mul x y := lmul x y -lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · simp - · simp only [map_add, hx₁, hx₂] +lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl -lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · simp - · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] +@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : + (tprod R x) * (tprod R y) = tprod R (x * y) := + lmul_tprod_tprod x y + +lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : + (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by + change lmul _ _ = _ + rw [map_smul, map_smul, mul_comm r s, mul_smul] + simp only [LinearMap.smul_apply, lmul_tprod_tprod] lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by induction' x using PiTensorProduct.induction_on <;> simp @@ -129,35 +124,68 @@ lemma lmul_add (x y z : ⨂[R] i, A i) : lmul x (y + z) = lmul x y + lmul x z := lemma add_lmul (x y z : ⨂[R] i, A i) : lmul (x + y) z = lmul x z + lmul y z := by induction' x using PiTensorProduct.induction_on <;> simp -instance mul : Mul (⨂[R] i, A i) where - mul x y := lmul x y +instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (⨂[R] i, A i) where + __ := mul + __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i)) + left_distrib := lmul_add + right_distrib := add_lmul + zero_mul := zero_lmul + mul_zero := lmul_zero -lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl +end NonUnitalNonAssocSemiring -@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : - (tprod R x) * (tprod R y) = tprod R (x * y) := - lmul_tprod_tprod x y +noncomputable section NonAssocSemiring -lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : - (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by - change lmul _ _ = _ - rw [map_smul, map_smul, mul_comm r s, mul_smul] - simp only [LinearMap.smul_apply, lmul_tprod_tprod] +variable [CommSemiring R] [∀ i, NonAssocSemiring (A i)] +variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] -instance monoid : Monoid (⨂[R] i, A i) where - __ := mul - __ := one - mul_assoc := lmul_assoc +lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · simp + · simp only [map_add, hx₁, hx₂] + +lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · simp + · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] + +instance nonAssocSemiring : NonAssocSemiring (⨂[R] i, A i) where + __ := nonUnitalNonAssocSemiring one_mul := one_lmul mul_one := lmul_one +end NonAssocSemiring + +noncomputable section NonUnitalSemiring + +variable [CommSemiring R] [∀ i, NonUnitalSemiring (A i)] +variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] + +lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by + induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ + · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ + · induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, mul_assoc] + · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ + rw [hz₁, hz₂] + · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ ⊢ + rw [hy₁, hy₂] + · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ + rw [hx₁, hx₂] + +instance nonUnitalSemiring : NonUnitalSemiring (⨂[R] i, A i) where + __ := nonUnitalNonAssocSemiring + mul_assoc := lmul_assoc + +end NonUnitalSemiring + +noncomputable section Semiring + +variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] + instance semiring : Semiring (⨂[R] i, A i) where - __ := monoid - __ := inferInstanceAs <| AddCommMonoidWithOne (⨂[R] i, A i) - left_distrib := lmul_add - right_distrib := add_lmul - zero_mul := zero_lmul - mul_zero := lmul_zero + __ := nonUnitalSemiring + __ := nonAssocSemiring instance algebra : Algebra R (⨂[R] i, A i) where __ := hasSMul' From 77a20f3b83f58efba3fcec70928e80f19a2f0af7 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Thu, 4 Jan 2024 18:25:45 +0000 Subject: [PATCH 16/60] Update PiTensorProduct.lean --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 96 +++++++++------------- 1 file changed, 41 insertions(+), 55 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index aeb6ff35d188c5..d4781066bd33e2 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -444,58 +444,61 @@ section variable (R M) -variable (s) in -/-- Re-index the components of the tensor power by `e`.-/ -def reindex (e : ι ≃ ι₂) : (⨂[R] i : ι, s i) ≃ₗ[R] ⨂[R] i : ι₂, s (e.symm i) := - let f := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s (e.symm i)) e - let g := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι), s i) e - LinearEquiv.ofLinear (lift <| f.symm <| tprod R) (lift <| g <| tprod R) (by aesop) (by aesop) +/-- Re-index the components of the tensor power by `e`. + +For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components. +-/ +def reindex (e : ι ≃ ι₂) : (⨂[R] _ : ι, M) ≃ₗ[R] ⨂[R] _ : ι₂, M := + LinearEquiv.ofLinear (lift (domDomCongr e.symm (tprod R : MultilinearMap R _ (⨂[R] _ : ι₂, M)))) + (lift (domDomCongr e (tprod R : MultilinearMap R _ (⨂[R] _ : ι, M)))) + (by + ext + simp only [LinearMap.comp_apply, LinearMap.id_apply, lift_tprod, + LinearMap.compMultilinearMap_apply, lift.tprod, domDomCongr_apply] + congr + ext + rw [e.apply_symm_apply]) + (by + ext + simp only [LinearMap.comp_apply, LinearMap.id_apply, lift_tprod, + LinearMap.compMultilinearMap_apply, lift.tprod, domDomCongr_apply] + congr + ext + rw [e.symm_apply_apply]) #align pi_tensor_product.reindex PiTensorProduct.reindex end @[simp] -theorem reindex_tprod (e : ι ≃ ι₂) (f : ∀ i, s i) : - reindex R s e (tprod R f) = tprod R fun i ↦ f (e.symm i) := by +theorem reindex_tprod (e : ι ≃ ι₂) (f : ∀ _, M) : + reindex R M e (tprod R f) = tprod R fun i ↦ f (e.symm i) := by dsimp [reindex] exact liftAux_tprod _ f #align pi_tensor_product.reindex_tprod PiTensorProduct.reindex_tprod @[simp] theorem reindex_comp_tprod (e : ι ≃ ι₂) : - (reindex R s e : (⨂[R] i : ι, s i) →ₗ[R] ⨂[R] i : ι₂, s (e.symm i)).compMultilinearMap - (tprod R) = - (domDomCongrLinearEquiv' R R s _ e).symm (tprod R) := + (reindex R M e : (⨂[R] _ : ι, M) →ₗ[R] ⨂[R] _ : ι₂, M).compMultilinearMap (tprod R) = + (tprod R : MultilinearMap R (fun _ ↦ M) _).domDomCongr e.symm := MultilinearMap.ext <| reindex_tprod e #align pi_tensor_product.reindex_comp_tprod PiTensorProduct.reindex_comp_tprod @[simp] -theorem lift_comp_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i ↦ s (e.symm i)) E) : - lift φ ∘ₗ (reindex R s e) = lift ((domDomCongrLinearEquiv' R R s _ e).symm φ) := by - ext; simp [reindex] +theorem lift_comp_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun _ : ι₂ ↦ M) E) : + lift φ ∘ₗ ↑(reindex R M e) = lift (φ.domDomCongr e.symm) := by + ext + simp #align pi_tensor_product.lift_comp_reindex PiTensorProduct.lift_comp_reindex @[simp] -theorem lift_comp_reindex_symm (e : ι ≃ ι₂) (φ : MultilinearMap R s E) : - lift φ ∘ₗ (reindex R s e).symm = lift (domDomCongrLinearEquiv' R R s _ e φ) := by - ext; simp [reindex] - -@[simp] -theorem lift_reindex - (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i ↦ s (e.symm i)) E) (x : ⨂[R] i, s i) : - lift φ (reindex R s e x) = lift ((domDomCongrLinearEquiv' R R s _ e).symm φ) x := +theorem lift_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun _ ↦ M) E) (x : ⨂[R] _, M) : + lift φ (reindex R M e x) = lift (φ.domDomCongr e.symm) x := LinearMap.congr_fun (lift_comp_reindex e φ) x #align pi_tensor_product.lift_reindex PiTensorProduct.lift_reindex -@[simp] -theorem lift_reindex_symm - (e : ι ≃ ι₂) (φ : MultilinearMap R s E) (x : ⨂[R] i, s (e.symm i)) : - lift φ (reindex R s e |>.symm x) = lift (domDomCongrLinearEquiv' R R s _ e φ) x := - LinearMap.congr_fun (lift_comp_reindex_symm e φ) x - @[simp] theorem reindex_trans (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) : - (reindex R s e).trans (reindex R _ e') = reindex R s (e.trans e') := by + (reindex R M e).trans (reindex R M e') = reindex R M (e.trans e') := by apply LinearEquiv.toLinearMap_injective ext f simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod, @@ -505,37 +508,21 @@ theorem reindex_trans (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) : #align pi_tensor_product.reindex_trans PiTensorProduct.reindex_trans @[simp] -theorem reindex_reindex (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) (x : ⨂[R] i, s i) : - reindex R _ e' (reindex R s e x) = reindex R s (e.trans e') x := - LinearEquiv.congr_fun (reindex_trans e e' : _ = reindex R s (e.trans e')) x +theorem reindex_reindex (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) (x : ⨂[R] _, M) : + reindex R M e' (reindex R M e x) = reindex R M (e.trans e') x := + LinearEquiv.congr_fun (reindex_trans e e' : _ = reindex R M (e.trans e')) x #align pi_tensor_product.reindex_reindex PiTensorProduct.reindex_reindex --- This doesn't have a dependent counterpart @[simp] -theorem reindex_symm (e : ι ≃ ι₂) : - (reindex R (fun i ↦ M) e).symm = reindex R (fun i ↦ M) e.symm := by - ext x - simp only [reindex, domDomCongrLinearEquiv', LinearEquiv.coe_symm_mk, LinearEquiv.coe_mk, - LinearEquiv.ofLinear_symm_apply, Equiv.symm_symm_apply, LinearEquiv.ofLinear_apply] - refine x.induction_on ?_ ?_ - · intro r x - simp only [map_smul, lift.tprod, coe_mk, comp_apply, Equiv.symm_symm_apply] - congr - ext y j - simp - · intro x y hx hy - rw [map_add, map_add, hx, hy] +theorem reindex_symm (e : ι ≃ ι₂) : (reindex R M e).symm = reindex R M e.symm := rfl #align pi_tensor_product.reindex_symm PiTensorProduct.reindex_symm @[simp] -theorem reindex_refl : reindex R s (Equiv.refl ι) = LinearEquiv.refl R _ := by +theorem reindex_refl : reindex R M (Equiv.refl ι) = LinearEquiv.refl R _ := by apply LinearEquiv.toLinearMap_injective ext - simp only [Equiv.refl_symm, Equiv.refl_apply, reindex, domDomCongrLinearEquiv', - LinearEquiv.coe_symm_mk, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, - LinearEquiv.refl_toLinearMap, LinearMap.id_coe, id_eq] - erw [lift.tprod] - congr + rw [reindex_comp_tprod, LinearEquiv.refl_toLinearMap, Equiv.refl_symm] + rfl #align pi_tensor_product.reindex_refl PiTensorProduct.reindex_refl variable (ι) @@ -543,7 +530,7 @@ variable (ι) attribute [local simp] eq_iff_true_of_subsingleton in /-- The tensor product over an empty index type `ι` is isomorphic to the base ring. -/ @[simps symm_apply] -def isEmptyEquiv [IsEmpty ι] : (⨂[R] i : ι, s i) ≃ₗ[R] R where +def isEmptyEquiv [IsEmpty ι] : (⨂[R] _ : ι, M) ≃ₗ[R] R where toFun := lift (constOfIsEmpty R _ 1) invFun r := r • tprod R (@isEmptyElim _ _ _) left_inv x := by @@ -564,8 +551,7 @@ def isEmptyEquiv [IsEmpty ι] : (⨂[R] i : ι, s i) ≃ₗ[R] R where #align pi_tensor_product.is_empty_equiv PiTensorProduct.isEmptyEquiv @[simp] -theorem isEmptyEquiv_apply_tprod [IsEmpty ι] (f : (i : ι) → s i) : - isEmptyEquiv ι (tprod R f) = 1 := +theorem isEmptyEquiv_apply_tprod [IsEmpty ι] (f : ι → M) : isEmptyEquiv ι (tprod R f) = 1 := lift.tprod _ #align pi_tensor_product.is_empty_equiv_apply_tprod PiTensorProduct.isEmptyEquiv_apply_tprod From a2364b951057ef8963672f74f68ac4da5083c72f Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Thu, 4 Jan 2024 18:26:34 +0000 Subject: [PATCH 17/60] Update TensorPower.lean --- Mathlib/LinearAlgebra/TensorPower.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean index a40c46ac1f5851..b742de299280fa 100644 --- a/Mathlib/LinearAlgebra/TensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorPower.lean @@ -52,8 +52,8 @@ are equal after a canonical reindexing. -/ @[ext] theorem gradedMonoid_eq_of_reindex_cast {ιι : Type*} {ι : ιι → Type*} : ∀ {a b : GradedMonoid fun ii => ⨂[R] _ : ι ii, M} (h : a.fst = b.fst), - reindex R (fun _ ↦ M) (Equiv.cast <| congr_arg ι h) a.snd = b.snd → a = b - | ⟨ai, a⟩, ⟨bi, b⟩ => fun (hi : ai = bi) (h : reindex R (fun _ ↦ M) _ a = b) => by + reindex R M (Equiv.cast <| congr_arg ι h) a.snd = b.snd → a = b + | ⟨ai, a⟩, ⟨bi, b⟩ => fun (hi : ai = bi) (h : reindex R M _ a = b) => by subst hi simp_all #align pi_tensor_product.graded_monoid_eq_of_reindex_cast PiTensorProduct.gradedMonoid_eq_of_reindex_cast @@ -78,7 +78,7 @@ theorem gOne_def : ₜ1 = tprod R (@Fin.elim0' M) := /-- A variant of `PiTensorProduct.tmulEquiv` with the result indexed by `Fin (n + m)`. -/ def mulEquiv {n m : ℕ} : (⨂[R]^n) M ⊗[R] (⨂[R]^m) M ≃ₗ[R] (⨂[R]^(n + m)) M := - (tmulEquiv R M).trans (reindex R (fun _ ↦ M) finSumFinEquiv) + (tmulEquiv R M).trans (reindex R M finSumFinEquiv) #align tensor_power.mul_equiv TensorPower.mulEquiv /-- As a graded monoid, `⨂[R]^i M` has a `(*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M`. -/ @@ -104,7 +104,7 @@ variable (R M) /-- Cast between "equal" tensor powers. -/ def cast {i j} (h : i = j) : (⨂[R]^i) M ≃ₗ[R] (⨂[R]^j) M := - reindex R (fun _ ↦ M) (Fin.castIso h).toEquiv + reindex R M (Fin.castIso h).toEquiv #align tensor_power.cast TensorPower.cast theorem cast_tprod {i j} (h : i = j) (a : Fin i → M) : @@ -114,8 +114,7 @@ theorem cast_tprod {i j} (h : i = j) (a : Fin i → M) : @[simp] theorem cast_refl {i} (h : i = i) : cast R M h = LinearEquiv.refl _ _ := - ((congr_arg fun f => reindex R (fun _ ↦ M) (RelIso.toEquiv f)) <| Fin.castIso_refl h).trans - reindex_refl + ((congr_arg fun f => reindex R M (RelIso.toEquiv f)) <| Fin.castIso_refl h).trans reindex_refl #align tensor_power.cast_refl TensorPower.cast_refl @[simp] From 4a3892afb984829ed88c44805924fcaa771e4c14 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Thu, 4 Jan 2024 18:27:13 +0000 Subject: [PATCH 18/60] Update ToTensorPower.lean --- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean index 21ea4f375cf15c..7cb1fcbf8a33e9 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean @@ -120,7 +120,7 @@ theorem ofDirectSum_toDirectSum (x : TensorAlgebra R M) : @[simp, nolint simpNF] -- see std4#365 for the simpNF issue theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m - (PiTensorProduct.reindex R (fun _ ↦ M) (Equiv.cast <| congr_arg Fin h) x) = + (PiTensorProduct.reindex R M (Equiv.cast <| congr_arg Fin h) x) = GradedMonoid.mk n x := Eq.symm (PiTensorProduct.gradedMonoid_eq_of_reindex_cast h rfl) #align tensor_algebra.mk_reindex_cast TensorAlgebra.mk_reindex_cast @@ -128,7 +128,7 @@ theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : @[simp] theorem mk_reindex_fin_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m - (PiTensorProduct.reindex R (fun _ ↦ M) (Fin.castIso h).toEquiv x) = GradedMonoid.mk n x := by + (PiTensorProduct.reindex R M (Fin.castIso h).toEquiv x) = GradedMonoid.mk n x := by rw [Fin.castIso_to_equiv, mk_reindex_cast h] #align tensor_algebra.mk_reindex_fin_cast TensorAlgebra.mk_reindex_fin_cast From e11b7bf8887e33e9ad15143768afda7962e67adb Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 12:49:10 +0000 Subject: [PATCH 19/60] add map --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 179 +++++++++++++++++++++ Mathlib/RingTheory/PiTensorProduct.lean | 53 +----- 2 files changed, 184 insertions(+), 48 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index d4781066bd33e2..81b19e211b8b2d 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -351,6 +351,8 @@ open MultilinearMap variable {s} +section lift + /-- Auxiliary function to constructing a linear map `(⨂[R] i, s i) → E` given a `MultilinearMap R s E` with the property that its composition with the canonical `MultilinearMap R s (⨂[R] i, s i)` is the given multilinear map. -/ @@ -440,6 +442,183 @@ theorem lift_tprod : lift (tprod R : MultilinearMap R s _) = LinearMap.id := Eq.symm <| lift.unique' rfl #align pi_tensor_product.lift_tprod PiTensorProduct.lift_tprod +end lift + +section map + +variable {t t' : ι → Type*} +variable [∀ i, AddCommMonoid (t i)] [∀ i, Module R (t i)] +variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)] + +/-- +Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: + +let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a family of `R`-linear map, then +`⨂ᵢ fᵢ` induces an `R`-linear map `F` between `R`-tensors `⨂ᵢ sᵢ` and `⨂ᵢ tᵢ` by +`F(⨂ aᵢ) = ⨂ f(aᵢ)`. +-/ +def mapAux (φ : ⨂[R] i, s i →ₗ[R] t i): + (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := + lift <| lift + (show MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) from + { toFun := fun f ↦ + { toFun := fun v ↦ tprod R fun j ↦ (f j) (v j) + map_add' := fun v i a b ↦ by + dsimp + simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i x j) = + update (fun k ↦ (f k) (v k)) i (f _ x) j by + · intro j x + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h], map_add, MultilinearMap.map_add] + map_smul' := fun v i r x ↦ by + dsimp + simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i (r • x) j) = + update (fun k ↦ (f k) (v k)) i (f _ (r • x)) j by + · intro j x + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h], map_smul, MultilinearMap.map_smul] + congr + ext j + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] } + map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by + dsimp + have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i z j (a j) = + update (fun i ↦ v i (a i)) i (z (a i)) j + · by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] + simp_rw [eq1] + erw [MultilinearMap.map_add] + map_smul' := fun v i r x ↦ MultilinearMap.ext <| fun a ↦ by + dsimp + have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i (r • z) j (a j) = + update (fun i ↦ v i (a i)) i (r • z (a i)) j + · by_cases h : j = i + · subst h; simp only [update_same, LinearMap.smul_apply] + · rw [update_noteq h, update_noteq h] + simp_rw [eq1] + erw [MultilinearMap.map_smul] + congr + ext j + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] }) φ + +lemma mapAux_tprod_tprod (f : ∀ i, s i →ₗ[R] t i) (x : ∀ i, s i) : + mapAux (tprod R f) (tprod R x) = tprod R (fun i ↦ f i (x i)) := by + delta mapAux + rw [lift.tprod, lift.tprod] + rfl + +lemma mapAux_add (φ ψ : ⨂[R] i, s i →ₗ[R] t i) : mapAux (φ + ψ) = mapAux φ + mapAux ψ := by + ext; simp [mapAux] + +lemma mapAux_smul (r : R) (φ : ⨂[R] i, s i →ₗ[R] t i) : mapAux (r • φ) = r • mapAux φ := by + ext; simp [mapAux] + +/-- +Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: + +let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a family of `R`-linear map, then +`⨂ᵢ fᵢ` induces an `R`-linear map `F` between `R`-tensors `⨂ᵢ sᵢ` and `⨂ᵢ tᵢ` by +`F(⨂ aᵢ) = ⨂ f(aᵢ)`. + +Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. +-/ +def map : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i where + toFun := mapAux + map_add' := mapAux_add + map_smul' := mapAux_smul + +@[simp] lemma map_tprod_tprod (f : ∀ i, s i →ₗ[R] t i) (x : ∀ i, s i) : + map (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [map, mapAux_tprod_tprod] + +/-- +Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: + +let `sᵢ` `tᵢ'` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ → tᵢ'` be a family of +`R`-linear map, then `⨂ᵢ fᵢ` induces an `R`-linear map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ ⊗ᵢ tᵢ'` by +`F(⨂ aᵢ, ⨂ bᵢ) = ⨂ f(aᵢ, bᵢ)`. +-/ +def map₂Aux (φ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : + (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) := + lift <| lift + (show MultilinearMap R (fun i ↦ s i →ₗ[R] t i →ₗ[R] t' i) + (MultilinearMap R s ((⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)) from + { toFun := fun v ↦ + { toFun := fun x ↦ map <| tprod R fun i ↦ v i (x i) + map_add' := fun x i a b ↦ by + dsimp + have eq1 (j : ι) (a : s i) : v j (update x i a j) = + update (fun i ↦ v i (x i)) i (v i a) j + · by_cases h : j = i + · subst h; simp + · rw [update_noteq h, update_noteq h] + simp_rw [eq1, map_add, MultilinearMap.map_add, map_add] + map_smul' := fun x i r a ↦ by + dsimp + have eq1 (j : ι) : v j (update x i (r • a) j) = + update (fun i ↦ v i (x i)) i (r • v i a) j + · by_cases h : j = i + · subst h; simp + · rw [update_noteq h, update_noteq h] + simp_rw [eq1, MultilinearMap.map_smul, map_smul] + congr + ext j b + by_cases h : j = i + · subst h; simp + · rw [update_noteq h, update_noteq h] } + map_add' := fun v i a a' ↦ MultilinearMap.ext fun b ↦ by + dsimp + have eq1 (j : ι) (a : s i →ₗ[R] t i →ₗ[R] t' i) : (update v i a j) (b j) = + update (fun i ↦ v i (b i)) i (a (b i)) j + · by_cases h : j = i + · subst h; simp + · rw [update_noteq h, update_noteq h] + simp_rw [eq1, LinearMap.add_apply, MultilinearMap.map_add, map_add] + map_smul' := fun v i r a ↦ MultilinearMap.ext fun b ↦ by + dsimp + have eq1 (j : ι) (a : s i →ₗ[R] t i →ₗ[R] t' i) : (update v i (r • a) j) (b j) = + update (fun i ↦ v i (b i)) i (r • a (b i)) j + · by_cases h : j = i + · subst h; simp + · rw [update_noteq h, update_noteq h] + simp_rw [eq1, MultilinearMap.map_smul, map_smul] + congr + ext j + by_cases h : j = i + · subst h; simp + · rw [update_noteq h, update_noteq h] }) φ + +lemma map₂Aux_tprod_tprod_tprod + (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : + map₂Aux (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by + simp [map₂Aux] + +lemma map₂Aux_add (φ ψ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : + map₂Aux (φ + ψ) = map₂Aux φ + map₂Aux ψ := by + ext; simp [map₂Aux] + +lemma map₂Aux_smul (r : R) (φ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : + map₂Aux (r • φ) = r • map₂Aux φ:= by + ext; simp [map₂Aux] + +def map₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] + (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) where + toFun := map₂Aux + map_add' := map₂Aux_add + map_smul' := map₂Aux_smul + +@[simp] lemma map₂_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : + map₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by + simp only [map₂, LinearMap.coe_mk, AddHom.coe_mk, map₂Aux_tprod_tprod_tprod] + +end map + section variable (R M) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index a5299c01e1da8e..a7017cf4c80e6f 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -41,61 +41,18 @@ noncomputable section NonUnitalNonAssocSemiring variable [CommSemiring R] [∀ i, NonUnitalNonAssocSemiring (A i)] variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] +attribute [aesop safe] mul_add mul_smul_comm smul_mul_assoc add_mul in /-- The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` -/ def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := -lift -{ toFun := fun x ↦ lift - { toFun := fun y ↦ tprod _ (x * y) - map_add' := fun z i a a' ↦ by - dsimp - rw [show x * update z i (a + a') = update (x * z) i (x i * (a + a')) by - · ext j - simp only [Pi.mul_apply, update] - aesop] - rw [mul_add, MultilinearMap.map_add] - congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop - map_smul' := fun z i r a ↦ by - dsimp - rw [show x * update z i (r • a) = update (x * z) i (r • (x i * a)) by - · ext j - simp only [Pi.mul_apply, update, mul_smul_comm] - split_ifs with h - · subst h; simp only; rw [mul_smul_comm] - · aesop] - rw [MultilinearMap.map_smul] - congr - ext j - simp only [update, Pi.mul_apply] - aesop } - map_add' := fun z i a a' ↦ by - ext z' - simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, - LinearMap.add_apply] - rw [show update z i (a + a') * z' = update (z * z') i ((a + a') * (z' i)) by - · ext j - simp only [Pi.mul_apply, update] - aesop] - rw [add_mul, MultilinearMap.map_add] - congr <;> ext j <;> simp only [update, Pi.mul_apply] <;> aesop - map_smul' := fun z i r a ↦ by - ext z' - simp only [LinearMap.compMultilinearMap_apply, lift.tprod, MultilinearMap.coe_mk, - LinearMap.smul_apply] - rw [show update z i (r • a) * z' = update (z * z') i ((r • a) * z' i) by - · ext j - simp only [Pi.mul_apply, update] - aesop] - rw [smul_mul_assoc, MultilinearMap.map_smul] - congr - ext j - simp only [update, Pi.mul_apply] - aesop } + PiTensorProduct.map₂ <| tprod R fun i ↦ by + refine ⟨⟨fun x ↦ ⟨⟨fun y ↦ x * y, ?_⟩, ?_⟩, ?_⟩, ?_⟩ <;> aesop @[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : lmul (tprod R x) (tprod R y) = tprod R (x * y) := by - simp only [lmul, lift.tprod, MultilinearMap.coe_mk] + simp only [lmul, map₂_tprod_tprod_tprod, LinearMap.coe_mk, AddHom.coe_mk] + rfl instance mul : Mul (⨂[R] i, A i) where mul x y := lmul x y From aae4fd999b17f32eded87ddfc8be80e37aae299a Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 13:02:37 +0000 Subject: [PATCH 20/60] =?UTF-8?q?=E6=9B=B4=E6=96=B0=20PiTensorProduct.lean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 81b19e211b8b2d..7f9511b8110db6 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -458,7 +458,7 @@ let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a f `F(⨂ aᵢ) = ⨂ f(aᵢ)`. -/ def mapAux (φ : ⨂[R] i, s i →ₗ[R] t i): - (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := + (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := lift <| lift (show MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) from { toFun := fun f ↦ From a0c52033d5caa32f45067d814102949e5f0c2c46 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 13:16:44 +0000 Subject: [PATCH 21/60] use LinearMap.mul --- Mathlib/RingTheory/PiTensorProduct.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index a7017cf4c80e6f..c65b8c466ea771 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -5,8 +5,7 @@ Authors: Jujian Zhang -/ import Mathlib.LinearAlgebra.PiTensorProduct -import Mathlib.Algebra.Algebra.Hom -import Mathlib.Algebra.Group.Pi +import Mathlib.Algebra.Algebra.Bilinear /-! # Tensor product of `R`-algebras and rings @@ -46,8 +45,7 @@ attribute [aesop safe] mul_add mul_smul_comm smul_mul_assoc add_mul in The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` -/ def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := - PiTensorProduct.map₂ <| tprod R fun i ↦ by - refine ⟨⟨fun x ↦ ⟨⟨fun y ↦ x * y, ?_⟩, ?_⟩, ?_⟩, ?_⟩ <;> aesop + PiTensorProduct.map₂ <| tprod R fun _ ↦ LinearMap.mul _ _ @[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : lmul (tprod R x) (tprod R y) = tprod R (x * y) := by From 01f77d29c2eb35de4ef4791f934762a8492748e3 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 13:32:50 +0000 Subject: [PATCH 22/60] golf --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 149 ++++++++------------- 1 file changed, 53 insertions(+), 96 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 7f9511b8110db6..5740882001f44e 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -450,6 +450,55 @@ variable {t t' : ι → Type*} variable [∀ i, AddCommMonoid (t i)] [∀ i, Module R (t i)] variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)] +variable (R s t) in +def _root_.MultilinearMap.piLinearMapToPiTensorProduct : + MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) := +{ toFun := fun f ↦ + { toFun := fun v ↦ tprod R fun j ↦ (f j) (v j) + map_add' := fun v i a b ↦ by + dsimp + simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i x j) = + update (fun k ↦ (f k) (v k)) i (f _ x) j by + · intro j x + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h], map_add, MultilinearMap.map_add] + map_smul' := fun v i r x ↦ by + dsimp + simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i (r • x) j) = + update (fun k ↦ (f k) (v k)) i (f _ (r • x)) j by + · intro j x + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h], map_smul, MultilinearMap.map_smul] + congr + ext j + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] } + map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by + dsimp + have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i z j (a j) = + update (fun i ↦ v i (a i)) i (z (a i)) j + · by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] + simp_rw [eq1] + erw [MultilinearMap.map_add] + map_smul' := fun v i r x ↦ MultilinearMap.ext <| fun a ↦ by + dsimp + have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i (r • z) j (a j) = + update (fun i ↦ v i (a i)) i (r • z (a i)) j + · by_cases h : j = i + · subst h; simp only [update_same, LinearMap.smul_apply] + · rw [update_noteq h, update_noteq h] + simp_rw [eq1] + erw [MultilinearMap.map_smul] + congr + ext j + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] } /-- Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: @@ -459,54 +508,7 @@ let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a f -/ def mapAux (φ : ⨂[R] i, s i →ₗ[R] t i): (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := - lift <| lift - (show MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) from - { toFun := fun f ↦ - { toFun := fun v ↦ tprod R fun j ↦ (f j) (v j) - map_add' := fun v i a b ↦ by - dsimp - simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i x j) = - update (fun k ↦ (f k) (v k)) i (f _ x) j by - · intro j x - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h], map_add, MultilinearMap.map_add] - map_smul' := fun v i r x ↦ by - dsimp - simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i (r • x) j) = - update (fun k ↦ (f k) (v k)) i (f _ (r • x)) j by - · intro j x - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h], map_smul, MultilinearMap.map_smul] - congr - ext j - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] } - map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by - dsimp - have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i z j (a j) = - update (fun i ↦ v i (a i)) i (z (a i)) j - · by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] - simp_rw [eq1] - erw [MultilinearMap.map_add] - map_smul' := fun v i r x ↦ MultilinearMap.ext <| fun a ↦ by - dsimp - have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i (r • z) j (a j) = - update (fun i ↦ v i (a i)) i (r • z (a i)) j - · by_cases h : j = i - · subst h; simp only [update_same, LinearMap.smul_apply] - · rw [update_noteq h, update_noteq h] - simp_rw [eq1] - erw [MultilinearMap.map_smul] - congr - ext j - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] }) φ + lift <| lift (MultilinearMap.piLinearMapToPiTensorProduct R s t) φ lemma mapAux_tprod_tprod (f : ∀ i, s i →ₗ[R] t i) (x : ∀ i, s i) : mapAux (tprod R f) (tprod R x) = tprod R (fun i ↦ f i (x i)) := by @@ -546,58 +548,13 @@ let `sᵢ` `tᵢ'` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ -/ def map₂Aux (φ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) := - lift <| lift - (show MultilinearMap R (fun i ↦ s i →ₗ[R] t i →ₗ[R] t' i) - (MultilinearMap R s ((⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)) from - { toFun := fun v ↦ - { toFun := fun x ↦ map <| tprod R fun i ↦ v i (x i) - map_add' := fun x i a b ↦ by - dsimp - have eq1 (j : ι) (a : s i) : v j (update x i a j) = - update (fun i ↦ v i (x i)) i (v i a) j - · by_cases h : j = i - · subst h; simp - · rw [update_noteq h, update_noteq h] - simp_rw [eq1, map_add, MultilinearMap.map_add, map_add] - map_smul' := fun x i r a ↦ by - dsimp - have eq1 (j : ι) : v j (update x i (r • a) j) = - update (fun i ↦ v i (x i)) i (r • v i a) j - · by_cases h : j = i - · subst h; simp - · rw [update_noteq h, update_noteq h] - simp_rw [eq1, MultilinearMap.map_smul, map_smul] - congr - ext j b - by_cases h : j = i - · subst h; simp - · rw [update_noteq h, update_noteq h] } - map_add' := fun v i a a' ↦ MultilinearMap.ext fun b ↦ by - dsimp - have eq1 (j : ι) (a : s i →ₗ[R] t i →ₗ[R] t' i) : (update v i a j) (b j) = - update (fun i ↦ v i (b i)) i (a (b i)) j - · by_cases h : j = i - · subst h; simp - · rw [update_noteq h, update_noteq h] - simp_rw [eq1, LinearMap.add_apply, MultilinearMap.map_add, map_add] - map_smul' := fun v i r a ↦ MultilinearMap.ext fun b ↦ by - dsimp - have eq1 (j : ι) (a : s i →ₗ[R] t i →ₗ[R] t' i) : (update v i (r • a) j) (b j) = - update (fun i ↦ v i (b i)) i (r • a (b i)) j - · by_cases h : j = i - · subst h; simp - · rw [update_noteq h, update_noteq h] - simp_rw [eq1, MultilinearMap.map_smul, map_smul] - congr - ext j - by_cases h : j = i - · subst h; simp - · rw [update_noteq h, update_noteq h] }) φ + lift <| LinearMap.compMultilinearMap map <| + (lift <| MultilinearMap.piLinearMapToPiTensorProduct R s _) φ lemma map₂Aux_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : map₂Aux (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by - simp [map₂Aux] + simp [map₂Aux, piLinearMapToPiTensorProduct] lemma map₂Aux_add (φ ψ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : map₂Aux (φ + ψ) = map₂Aux φ + map₂Aux ψ := by From 04daa42d13686051453db852b4242b3381079ca9 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 13:33:56 +0000 Subject: [PATCH 23/60] Update Mathlib/LinearAlgebra/PiTensorProduct.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 5740882001f44e..27b825a2e164e7 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -452,7 +452,7 @@ variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)] variable (R s t) in def _root_.MultilinearMap.piLinearMapToPiTensorProduct : - MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) := + MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) := { toFun := fun f ↦ { toFun := fun v ↦ tprod R fun j ↦ (f j) (v j) map_add' := fun v i a b ↦ by From e9847be38392649e8cd1f21034a669852510e705 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 13:55:53 +0000 Subject: [PATCH 24/60] golf and rename --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 70 ++++++---------------- 1 file changed, 18 insertions(+), 52 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 5740882001f44e..99365708273b82 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -451,6 +451,7 @@ variable [∀ i, AddCommMonoid (t i)] [∀ i, Module R (t i)] variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)] variable (R s t) in +@[simps] def _root_.MultilinearMap.piLinearMapToPiTensorProduct : MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) := { toFun := fun f ↦ @@ -499,28 +500,6 @@ def _root_.MultilinearMap.piLinearMapToPiTensorProduct : by_cases h : j = i · subst h; simp only [update_same] · rw [update_noteq h, update_noteq h] } -/-- -Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: - -let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a family of `R`-linear map, then -`⨂ᵢ fᵢ` induces an `R`-linear map `F` between `R`-tensors `⨂ᵢ sᵢ` and `⨂ᵢ tᵢ` by -`F(⨂ aᵢ) = ⨂ f(aᵢ)`. --/ -def mapAux (φ : ⨂[R] i, s i →ₗ[R] t i): - (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := - lift <| lift (MultilinearMap.piLinearMapToPiTensorProduct R s t) φ - -lemma mapAux_tprod_tprod (f : ∀ i, s i →ₗ[R] t i) (x : ∀ i, s i) : - mapAux (tprod R f) (tprod R x) = tprod R (fun i ↦ f i (x i)) := by - delta mapAux - rw [lift.tprod, lift.tprod] - rfl - -lemma mapAux_add (φ ψ : ⨂[R] i, s i →ₗ[R] t i) : mapAux (φ + ψ) = mapAux φ + mapAux ψ := by - ext; simp [mapAux] - -lemma mapAux_smul (r : R) (φ : ⨂[R] i, s i →ₗ[R] t i) : mapAux (r • φ) = r • mapAux φ := by - ext; simp [mapAux] /-- Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: @@ -531,13 +510,14 @@ let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a f Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. -/ -def map : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i where - toFun := mapAux - map_add' := mapAux_add - map_smul' := mapAux_smul +def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i where + toFun φ := lift <| lift (MultilinearMap.piLinearMapToPiTensorProduct R s t) φ + map_add' _ _ := by ext; simp + map_smul' _ _ := by ext; simp -@[simp] lemma map_tprod_tprod (f : ∀ i, s i →ₗ[R] t i) (x : ∀ i, s i) : - map (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [map, mapAux_tprod_tprod] +@[simp] lemma piTensorHomMap_tprod_tprod (f : ∀ i, s i →ₗ[R] t i) (x : ∀ i, s i) : + piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by + simp [piTensorHomMap] /-- Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: @@ -545,34 +525,20 @@ Arbitrary tensor product of linear maps to linear maps between arbitrary tensor let `sᵢ` `tᵢ'` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ → tᵢ'` be a family of `R`-linear map, then `⨂ᵢ fᵢ` induces an `R`-linear map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ ⊗ᵢ tᵢ'` by `F(⨂ aᵢ, ⨂ bᵢ) = ⨂ f(aᵢ, bᵢ)`. + +Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. -/ -def map₂Aux (φ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : - (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) := - lift <| LinearMap.compMultilinearMap map <| +def piTensorHomMap₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] + (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) where + toFun φ := lift <| LinearMap.compMultilinearMap piTensorHomMap <| (lift <| MultilinearMap.piLinearMapToPiTensorProduct R s _) φ + map_add' _ _ := by ext; simp + map_smul' _ _ := by ext; simp -lemma map₂Aux_tprod_tprod_tprod +@[simp] lemma piTensorHomMap₂_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : - map₂Aux (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by - simp [map₂Aux, piLinearMapToPiTensorProduct] - -lemma map₂Aux_add (φ ψ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : - map₂Aux (φ + ψ) = map₂Aux φ + map₂Aux ψ := by - ext; simp [map₂Aux] - -lemma map₂Aux_smul (r : R) (φ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) : - map₂Aux (r • φ) = r • map₂Aux φ:= by - ext; simp [map₂Aux] - -def map₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] - (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) where - toFun := map₂Aux - map_add' := map₂Aux_add - map_smul' := map₂Aux_smul - -@[simp] lemma map₂_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : - map₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by - simp only [map₂, LinearMap.coe_mk, AddHom.coe_mk, map₂Aux_tprod_tprod_tprod] + piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by + simp [piTensorHomMap₂] end map From fdf208d86b43e0ce1c0a87a76d86a7c3b3b26384 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 14:06:02 +0000 Subject: [PATCH 25/60] fix --- Mathlib/RingTheory/PiTensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index c65b8c466ea771..247d41c897f0f8 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -45,11 +45,11 @@ attribute [aesop safe] mul_add mul_smul_comm smul_mul_assoc add_mul in The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` -/ def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := - PiTensorProduct.map₂ <| tprod R fun _ ↦ LinearMap.mul _ _ + PiTensorProduct.piTensorHomMap₂ <| tprod R fun _ ↦ LinearMap.mul _ _ @[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : lmul (tprod R x) (tprod R y) = tprod R (x * y) := by - simp only [lmul, map₂_tprod_tprod_tprod, LinearMap.coe_mk, AddHom.coe_mk] + simp only [lmul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply'] rfl instance mul : Mul (⨂[R] i, A i) where From 82c54bc0cdaaa7ad011fe67aacaeda280043b340 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 14:24:27 +0000 Subject: [PATCH 26/60] add map --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index c749d1bd8fcfd0..1a3aadad68e02a 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -501,6 +501,13 @@ def _root_.MultilinearMap.piLinearMapToPiTensorProduct : · subst h; simp only [update_same] · rw [update_noteq h, update_noteq h] } +def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := + lift <| MultilinearMap.piLinearMapToPiTensorProduct _ _ _ f + +@[simp] lemma map_tprod (f : Π i, s i →ₗ[R] t i) (x : ∀ i, s i) : + map f (tprod R x) = tprod R fun i ↦ f i (x i) := + lift.tprod _ + /-- Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: From d693761e0dda64ca299a9f77ba932a3fd442dac6 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 14:28:17 +0000 Subject: [PATCH 27/60] add map2 --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 1a3aadad68e02a..a17cf0eda4765d 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -526,6 +526,15 @@ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) → piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [piTensorHomMap] +def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : + (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:= + lift <| LinearMap.compMultilinearMap piTensorHomMap <| + MultilinearMap.piLinearMapToPiTensorProduct _ _ _ f + +lemma map₂_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : ∀ i, s i) (y : ∀ i, t i) : + map₂ f (tprod R x) (tprod R y) = tprod R fun i ↦ f i (x i) (y i) := by + simp [map₂] + /-- Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: From 8c94b128319b9bceecedca2e8f9835e91ae5007b Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 14:47:08 +0000 Subject: [PATCH 28/60] add a lemma --- Mathlib/RingTheory/PiTensorProduct.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 247d41c897f0f8..a6c78cb59d0503 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -166,6 +166,13 @@ instance algebra : Algebra R (⨂[R] i, A i) where change _ = r • (1 * x) rw [one_mul] +lemma algebraMap_apply (r : R) (i : ι) [DecidableEq ι] : + algebraMap R (⨂[R] i, A i) r = tprod R (Pi.mulSingle i (algebraMap R (A i) r)) := by + change r • tprod R 1 = _ + rw [show Pi.mulSingle i (algebraMap R (A i) r) = update (fun i ↦ 1) i (r • 1) by + · rw [Algebra.algebraMap_eq_smul_one]; rfl, MultilinearMap.map_smul, update_eq_self] + congr + /-- the map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` -/ From 61d2c036691f5bc997e8c49d6ca04373e3aaa57e Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 14:56:06 +0000 Subject: [PATCH 29/60] add docs --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index a17cf0eda4765d..fcf87472bf0f23 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -451,6 +451,11 @@ variable [∀ i, AddCommMonoid (t i)] [∀ i, Module R (t i)] variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)] variable (R s t) in + +/-- +Let `sᵢ` and `tᵢ` be family of `R`-modules, a map from `Π i, sᵢ → tᵢ` to multilinear maps +`(Π i, sᵢ) → ⨂ tᵢ` by `(fᵢ) ↦ v ↦ ⨂ₜ fᵢ vᵢ`. This map is multilinear as well. +-/ @[simps] def _root_.MultilinearMap.piLinearMapToPiTensorProduct : MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) := @@ -501,6 +506,10 @@ def _root_.MultilinearMap.piLinearMapToPiTensorProduct : · subst h; simp only [update_same] · rw [update_noteq h, update_noteq h] } +/-- +let `sᵢ` and `tᵢ` be family of `R`-modules and a family `fᵢ` of `R`-linear maps `sᵢ → tᵢ`, then +there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`. +-/ def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := lift <| MultilinearMap.piLinearMapToPiTensorProduct _ _ _ f @@ -526,6 +535,11 @@ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) → piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [piTensorHomMap] +/-- +let `sᵢ`, `tᵢ` and `tᵢ'` be family of `R`-modules and a family `fᵢ` of `R`-linear maps +`sᵢ → tᵢ → tᵢ'`, then there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ → ⨂ᵢ tᵢ'` by +`⨂ aᵢ ↦⨂ bᵢ ↦ ⨂ fᵢ aᵢ bᵢ`. +-/ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:= lift <| LinearMap.compMultilinearMap piTensorHomMap <| From f4e668abd6380eac9488a98de53573f359adedb9 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 15:38:58 +0000 Subject: [PATCH 30/60] =?UTF-8?q?=E6=9B=B4=E6=96=B0=20PiTensorProduct.lean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index fcf87472bf0f23..c5137c38e1b7d0 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -509,6 +509,8 @@ def _root_.MultilinearMap.piLinearMapToPiTensorProduct : /-- let `sᵢ` and `tᵢ` be family of `R`-modules and a family `fᵢ` of `R`-linear maps `sᵢ → tᵢ`, then there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`. + +This is `TensorProduct.map` for an arbitrary family of modules. -/ def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := lift <| MultilinearMap.piLinearMapToPiTensorProduct _ _ _ f @@ -525,6 +527,8 @@ let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a f `F(⨂ aᵢ) = ⨂ f(aᵢ)`. Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. + +This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules. -/ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i where toFun φ := lift <| lift (MultilinearMap.piLinearMapToPiTensorProduct R s t) φ @@ -538,7 +542,9 @@ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) → /-- let `sᵢ`, `tᵢ` and `tᵢ'` be family of `R`-modules and a family `fᵢ` of `R`-linear maps `sᵢ → tᵢ → tᵢ'`, then there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ → ⨂ᵢ tᵢ'` by -`⨂ aᵢ ↦⨂ bᵢ ↦ ⨂ fᵢ aᵢ bᵢ`. +`⨂ aᵢ ↦ ⨂ bᵢ ↦ ⨂ fᵢ aᵢ bᵢ`. + +This is `TensorProduct.map` for two arbitrary families of modules. -/ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:= @@ -557,6 +563,8 @@ let `sᵢ` `tᵢ'` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ `F(⨂ aᵢ, ⨂ bᵢ) = ⨂ f(aᵢ, bᵢ)`. Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. + +This is `TensorProduct.homTensorHomMap` for two arbitrary families of modules. -/ def piTensorHomMap₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) where From 06b91fffe37252c535aff58bb120ab183c10a0fd Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 16:38:28 +0000 Subject: [PATCH 31/60] Update Mathlib/LinearAlgebra/PiTensorProduct.lean Co-authored-by: Eric Wieser --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 24 +--------------------- 1 file changed, 1 insertion(+), 23 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index c5137c38e1b7d0..fea99fb37b104d 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -459,29 +459,7 @@ Let `sᵢ` and `tᵢ` be family of `R`-modules, a map from `Π i, sᵢ → tᵢ` @[simps] def _root_.MultilinearMap.piLinearMapToPiTensorProduct : MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) := -{ toFun := fun f ↦ - { toFun := fun v ↦ tprod R fun j ↦ (f j) (v j) - map_add' := fun v i a b ↦ by - dsimp - simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i x j) = - update (fun k ↦ (f k) (v k)) i (f _ x) j by - · intro j x - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h], map_add, MultilinearMap.map_add] - map_smul' := fun v i r x ↦ by - dsimp - simp_rw [show ∀ (j : ι) (x : s i), (f j) (update v i (r • x) j) = - update (fun k ↦ (f k) (v k)) i (f _ (r • x)) j by - · intro j x - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h], map_smul, MultilinearMap.map_smul] - congr - ext j - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] } +{ toFun := (tprod R).compLinearMap map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by dsimp have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i z j (a j) = From e8a20076df77c815272f6082b591592f5ebb68e6 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 16:38:43 +0000 Subject: [PATCH 32/60] Update Mathlib/LinearAlgebra/PiTensorProduct.lean Co-authored-by: Eric Wieser --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index fea99fb37b104d..437dc61db397aa 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -491,7 +491,7 @@ there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ f This is `TensorProduct.map` for an arbitrary family of modules. -/ def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := - lift <| MultilinearMap.piLinearMapToPiTensorProduct _ _ _ f + lift <| (tprod R).compLinearMap f @[simp] lemma map_tprod (f : Π i, s i →ₗ[R] t i) (x : ∀ i, s i) : map f (tprod R x) = tprod R fun i ↦ f i (x i) := From 1cdc12255678e1b3bcd9f12dac09b847d776bd90 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 16:41:29 +0000 Subject: [PATCH 33/60] apply suggestions by @eric-wieser --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 437dc61db397aa..5acb04d4834ac8 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -526,8 +526,7 @@ This is `TensorProduct.map` for two arbitrary families of modules. -/ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:= - lift <| LinearMap.compMultilinearMap piTensorHomMap <| - MultilinearMap.piLinearMapToPiTensorProduct _ _ _ f + lift <| LinearMap.compMultilinearMap piTensorHomMap <| (tprod R).compLinearMap f lemma map₂_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : ∀ i, s i) (y : ∀ i, t i) : map₂ f (tprod R x) (tprod R y) = tprod R fun i ↦ f i (x i) (y i) := by From deaf5153f4eea966bf71851f298d0019b501d4db Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 17:05:24 +0000 Subject: [PATCH 34/60] add a new multilineaar map --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 32 +++++++++++++++ Mathlib/LinearAlgebra/PiTensorProduct.lean | 42 ++------------------ 2 files changed, 36 insertions(+), 38 deletions(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 6fb14148bba21e..99daa227624bad 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -949,6 +949,38 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g map_add' := fun _ _ ↦ rfl map_smul' := fun _ _ ↦ rfl +/-- +If `g` is a multilinear map from `(M₁')ᵢ` to `M₂`, then `g` can be reinterpreted as a multilinear +map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(fᵢ) ↦ v ↦ ⨂ₜ fᵢ vᵢ`. +-/ +@[simps] +def piLinearMap (g : MultilinearMap R M₁' M₂) : + MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := +{ toFun := g.compLinearMap + map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by + dsimp + have eq1 (j : ι) (z : M₁ i →ₗ[R] M₁' i) : update v i z j (a j) = + update (fun i ↦ v i (a i)) i (z (a i)) j + · by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] + simp_rw [eq1] + erw [MultilinearMap.map_add] + map_smul' := fun v i r x ↦ MultilinearMap.ext <| fun a ↦ by + dsimp + have eq1 (j : ι) (z : M₁ i →ₗ[R] M₁' i) : update v i (r • z) j (a j) = + update (fun i ↦ v i (a i)) i (r • z (a i)) j + · by_cases h : j = i + · subst h; simp only [update_same, LinearMap.smul_apply] + · rw [update_noteq h, update_noteq h] + simp_rw [eq1] + erw [MultilinearMap.map_smul] + congr + ext j + by_cases h : j = i + · subst h; simp only [update_same] + · rw [update_noteq h, update_noteq h] } + /-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap` sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g` and multilinear in `f₁, ..., fₙ`. -/ diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 5acb04d4834ac8..49f661acaad81a 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -450,40 +450,6 @@ variable {t t' : ι → Type*} variable [∀ i, AddCommMonoid (t i)] [∀ i, Module R (t i)] variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)] -variable (R s t) in - -/-- -Let `sᵢ` and `tᵢ` be family of `R`-modules, a map from `Π i, sᵢ → tᵢ` to multilinear maps -`(Π i, sᵢ) → ⨂ tᵢ` by `(fᵢ) ↦ v ↦ ⨂ₜ fᵢ vᵢ`. This map is multilinear as well. --/ -@[simps] -def _root_.MultilinearMap.piLinearMapToPiTensorProduct : - MultilinearMap R (fun i ↦ s i →ₗ[R] t i) (MultilinearMap R s (⨂[R] (i : ι), t i)) := -{ toFun := (tprod R).compLinearMap - map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by - dsimp - have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i z j (a j) = - update (fun i ↦ v i (a i)) i (z (a i)) j - · by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] - simp_rw [eq1] - erw [MultilinearMap.map_add] - map_smul' := fun v i r x ↦ MultilinearMap.ext <| fun a ↦ by - dsimp - have eq1 (j : ι) (z : s i →ₗ[R] t i) : update v i (r • z) j (a j) = - update (fun i ↦ v i (a i)) i (r • z (a i)) j - · by_cases h : j = i - · subst h; simp only [update_same, LinearMap.smul_apply] - · rw [update_noteq h, update_noteq h] - simp_rw [eq1] - erw [MultilinearMap.map_smul] - congr - ext j - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] } - /-- let `sᵢ` and `tᵢ` be family of `R`-modules and a family `fᵢ` of `R`-linear maps `sᵢ → tᵢ`, then there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`. @@ -509,7 +475,7 @@ Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules. -/ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i where - toFun φ := lift <| lift (MultilinearMap.piLinearMapToPiTensorProduct R s t) φ + toFun φ := lift <| lift (MultilinearMap.piLinearMap <| tprod R) φ map_add' _ _ := by ext; simp map_smul' _ _ := by ext; simp @@ -546,9 +512,9 @@ This is `TensorProduct.homTensorHomMap` for two arbitrary families of modules. def piTensorHomMap₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) where toFun φ := lift <| LinearMap.compMultilinearMap piTensorHomMap <| - (lift <| MultilinearMap.piLinearMapToPiTensorProduct R s _) φ - map_add' _ _ := by ext; simp - map_smul' _ _ := by ext; simp + (lift <| MultilinearMap.piLinearMap <| tprod R) φ + map_add' x y := by dsimp; ext; simp + map_smul' r x := by dsimp; ext; simp @[simp] lemma piTensorHomMap₂_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : From 9edb831687b2e49a47f20fd437b869a962cec3e7 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 17:06:19 +0000 Subject: [PATCH 35/60] Update Mathlib/LinearAlgebra/Multilinear/Basic.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 99daa227624bad..9269be7479288a 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -955,7 +955,7 @@ map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(f -/ @[simps] def piLinearMap (g : MultilinearMap R M₁' M₂) : - MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := + MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := { toFun := g.compLinearMap map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by dsimp From f9a3f2c415d8f2081dbe7da154e75dde81d07335 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 17:07:23 +0000 Subject: [PATCH 36/60] Update Basic.lean --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 9269be7479288a..66426f7e62d784 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -951,7 +951,7 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g /-- If `g` is a multilinear map from `(M₁')ᵢ` to `M₂`, then `g` can be reinterpreted as a multilinear -map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(fᵢ) ↦ v ↦ ⨂ₜ fᵢ vᵢ`. +map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(fᵢ) ↦ v ↦ g (fᵢ vᵢ)`. -/ @[simps] def piLinearMap (g : MultilinearMap R M₁' M₂) : From b4bfd52d3e5ef2692a478d58f3324b86b6cca05e Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 17:10:15 +0000 Subject: [PATCH 37/60] use eric's solution --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 41 +++++--------------- 1 file changed, 9 insertions(+), 32 deletions(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 99daa227624bad..703f5c2e0051a5 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -949,38 +949,6 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g map_add' := fun _ _ ↦ rfl map_smul' := fun _ _ ↦ rfl -/-- -If `g` is a multilinear map from `(M₁')ᵢ` to `M₂`, then `g` can be reinterpreted as a multilinear -map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(fᵢ) ↦ v ↦ ⨂ₜ fᵢ vᵢ`. --/ -@[simps] -def piLinearMap (g : MultilinearMap R M₁' M₂) : - MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := -{ toFun := g.compLinearMap - map_add' := fun v i x y ↦ MultilinearMap.ext <| fun a ↦ by - dsimp - have eq1 (j : ι) (z : M₁ i →ₗ[R] M₁' i) : update v i z j (a j) = - update (fun i ↦ v i (a i)) i (z (a i)) j - · by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] - simp_rw [eq1] - erw [MultilinearMap.map_add] - map_smul' := fun v i r x ↦ MultilinearMap.ext <| fun a ↦ by - dsimp - have eq1 (j : ι) (z : M₁ i →ₗ[R] M₁' i) : update v i (r • z) j (a j) = - update (fun i ↦ v i (a i)) i (r • z (a i)) j - · by_cases h : j = i - · subst h; simp only [update_same, LinearMap.smul_apply] - · rw [update_noteq h, update_noteq h] - simp_rw [eq1] - erw [MultilinearMap.map_smul] - congr - ext j - by_cases h : j = i - · subst h; simp only [update_same] - · rw [update_noteq h, update_noteq h] } - /-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap` sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g` and multilinear in `f₁, ..., fₙ`. -/ @@ -1007,6 +975,15 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g · exact Function.apply_update c f i (a • f₀) j · exact Function.apply_update c f i f₀ j +/-- +If `g` is a multilinear map from `(M₁')ᵢ` to `M₂`, then `g` can be reinterpreted as a multilinear +map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. +-/ +@[simps] +def piLinearMap (g : MultilinearMap R M₁' M₂) : + MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := +(LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear + end /-- If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear From d5e04c02f50e666592ced551bcaf099dff263a66 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 17:11:56 +0000 Subject: [PATCH 38/60] Update Mathlib/LinearAlgebra/Multilinear/Basic.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 703f5c2e0051a5..f800b05ee8e25e 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -981,7 +981,7 @@ map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(f -/ @[simps] def piLinearMap (g : MultilinearMap R M₁' M₂) : - MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := + MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear end From 5ee71ecc74cc988fbd738bcc4eaba1b65a4ac3e7 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 17:20:41 +0000 Subject: [PATCH 39/60] better docs --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 703f5c2e0051a5..f81b4e6a45550d 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -976,13 +976,18 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g · exact Function.apply_update c f i f₀ j /-- -If `g` is a multilinear map from `(M₁')ᵢ` to `M₂`, then `g` can be reinterpreted as a multilinear -map of multilinear map from `(M₁ ⟶ M₁')ᵢ` to `(M₁)ᵢ ⟶ M₂` by `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. +Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module. Let us denote `M` and +`M'` to be `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` respectively. +If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear +map of multilinear map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` by `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. -/ -@[simps] +@[simps!] def piLinearMap (g : MultilinearMap R M₁' M₂) : - MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) := -(LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear + MultilinearMap R M₁' M₂ →ₗ[R] + MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) where + toFun g := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear + map_add' := by aesop + map_smul' := by aesop end From a852f1f9b2c32bdab894cd88edb273ca14a70ab2 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 17:23:25 +0000 Subject: [PATCH 40/60] =?UTF-8?q?=E6=9B=B4=E6=96=B0=20Basic.lean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index bd1cef65eeedb3..7a145d261b1a72 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -983,7 +983,7 @@ map of multilinear map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` by `(f -/ @[simps!] def piLinearMap : - MultilinearMap R M₁' M₂ →ₗ[R] + MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) where toFun g := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear map_add' := by aesop From 9cad6662cc53cfb37ab3080ebbe9c18b083198f3 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 8 Jan 2024 18:06:27 +0000 Subject: [PATCH 41/60] =?UTF-8?q?=E6=9B=B4=E6=96=B0=20Basic.lean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 7a145d261b1a72..81de0a0543bd2e 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -981,8 +981,7 @@ Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-mo If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear map of multilinear map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` by `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. -/ -@[simps!] -def piLinearMap : +@[simps!] def piLinearMap : MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) where toFun g := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear From ba1f2fa94e7027daafdd6eddfdd0b6640f5a9b0b Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 20 Feb 2024 13:20:27 +0000 Subject: [PATCH 42/60] Update Mathlib/LinearAlgebra/Multilinear/Basic.lean Co-authored-by: Riccardo Brasca --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 91999fb6f06535..9082adb6dadba4 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -1041,8 +1041,8 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g · exact Function.apply_update c f i f₀ j /-- -Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module. Let us denote `M` and -`M'` to be `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` respectively. +Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module. Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and +`M'` respectively. If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear map of multilinear map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` by `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. -/ From 2a0b0c04730fa0653ac6bb13c715b85e44900fdb Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 20 Feb 2024 14:04:00 +0000 Subject: [PATCH 43/60] docs fix in `PiTensorProduct` --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 40 +++++++++------------- 1 file changed, 17 insertions(+), 23 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index a27cffd44e861b..c119f1577fed56 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -452,42 +452,40 @@ variable [∀ i, AddCommMonoid (t i)] [∀ i, Module R (t i)] variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)] /-- -let `sᵢ` and `tᵢ` be family of `R`-modules and a family `fᵢ` of `R`-linear maps `sᵢ → tᵢ`, then -there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`. +Let `sᵢ` and `tᵢ` be two families of `R`-modules. +Let `f` be a family of `R`-linear maps between `sᵢ` and `tᵢ`, i.e. `f : Πᵢ sᵢ → tᵢ`, +then there is an induced map `⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`. This is `TensorProduct.map` for an arbitrary family of modules. -/ def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := lift <| (tprod R).compLinearMap f -@[simp] lemma map_tprod (f : Π i, s i →ₗ[R] t i) (x : ∀ i, s i) : +@[simp] lemma map_apply_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) : map f (tprod R x) = tprod R fun i ↦ f i (x i) := lift.tprod _ /-- -Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: - -let `sᵢ` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ` be a family of `R`-linear map, then -`⨂ᵢ fᵢ` induces an `R`-linear map `F` between `R`-tensors `⨂ᵢ sᵢ` and `⨂ᵢ tᵢ` by -`F(⨂ aᵢ) = ⨂ f(aᵢ)`. - -Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. +Let `sᵢ` and `tᵢ` be families of `R`-modules. +Then there is an `R`=linear map between `⨂ᵢ Hom(sᵢ, tᵢ)` and `Hom(⨂ᵢ sᵢ, ⨂ tᵢ)` defined by +`⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ fᵢ aᵢ`. This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules. + +Note that `PiTensorProduct.piTensorHomMap (tprod R f)` is equal to `PiTensorProduct.map f`. -/ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i where toFun φ := lift <| lift (MultilinearMap.piLinearMap <| tprod R) φ map_add' _ _ := by ext; simp map_smul' _ _ := by ext; simp -@[simp] lemma piTensorHomMap_tprod_tprod (f : ∀ i, s i →ₗ[R] t i) (x : ∀ i, s i) : +@[simp] lemma piTensorHomMap_apply_tprod_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) : piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [piTensorHomMap] /-- -let `sᵢ`, `tᵢ` and `tᵢ'` be family of `R`-modules and a family `fᵢ` of `R`-linear maps -`sᵢ → tᵢ → tᵢ'`, then there is an induced map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ → ⨂ᵢ tᵢ'` by -`⨂ aᵢ ↦ ⨂ bᵢ ↦ ⨂ fᵢ aᵢ bᵢ`. +Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, i.e. `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an +element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`. This is `TensorProduct.map` for two arbitrary families of modules. -/ @@ -495,18 +493,14 @@ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:= lift <| LinearMap.compMultilinearMap piTensorHomMap <| (tprod R).compLinearMap f -lemma map₂_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : ∀ i, s i) (y : ∀ i, t i) : +lemma map₂_apply_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : Π i, s i) (y : Π i, t i) : map₂ f (tprod R x) (tprod R y) = tprod R fun i ↦ f i (x i) (y i) := by simp [map₂] /-- -Arbitrary tensor product of linear maps to linear maps between arbitrary tensor products: - -let `sᵢ` `tᵢ'` and `tᵢ` be family of `R`-modules and `fᵢ : sᵢ → tᵢ → tᵢ'` be a family of -`R`-linear map, then `⨂ᵢ fᵢ` induces an `R`-linear map `F : ⨂ᵢ sᵢ → ⨂ᵢ tᵢ ⊗ᵢ tᵢ'` by -`F(⨂ aᵢ, ⨂ bᵢ) = ⨂ f(aᵢ, bᵢ)`. - -Furthermore, the map `⨂ᵢ fᵢ ↦ F` is `R`-linear as well. +Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules. +Then there is an linear map from `⨂ᵢ Hom(sᵢ, Hom(tᵢ, t'ᵢ))` to `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` +defined by `⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`. This is `TensorProduct.homTensorHomMap` for two arbitrary families of modules. -/ @@ -517,7 +511,7 @@ def piTensorHomMap₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] map_add' x y := by dsimp; ext; simp map_smul' r x := by dsimp; ext; simp -@[simp] lemma piTensorHomMap₂_tprod_tprod_tprod +@[simp] lemma piTensorHomMap₂_apply_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by simp [piTensorHomMap₂] From 278fccaa5282e092a729ff97f32c11f76fc19581 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 20 Feb 2024 14:30:13 +0000 Subject: [PATCH 44/60] induction' -> induction --- Mathlib/RingTheory/PiTensorProduct.lean | 85 ++++++++++++++----------- 1 file changed, 49 insertions(+), 36 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index a6c78cb59d0503..47e1a635566c05 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -68,16 +68,16 @@ lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : simp only [LinearMap.smul_apply, lmul_tprod_tprod] lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by - induction' x using PiTensorProduct.induction_on <;> simp + induction x using PiTensorProduct.induction_on <;> simp lemma lmul_zero (x : ⨂[R] i, A i) : lmul x 0 = 0 := by - induction' x using PiTensorProduct.induction_on <;> simp + induction x using PiTensorProduct.induction_on <;> simp lemma lmul_add (x y z : ⨂[R] i, A i) : lmul x (y + z) = lmul x y + lmul x z := by - induction' x using PiTensorProduct.induction_on <;> simp + induction x using PiTensorProduct.induction_on <;> simp lemma add_lmul (x y z : ⨂[R] i, A i) : lmul (x + y) z = lmul x z + lmul y z := by - induction' x using PiTensorProduct.induction_on <;> simp + induction x using PiTensorProduct.induction_on <;> simp instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (⨂[R] i, A i) where __ := mul @@ -95,14 +95,14 @@ variable [CommSemiring R] [∀ i, NonAssocSemiring (A i)] variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · simp - · simp only [map_add, hx₁, hx₂] + induction x using PiTensorProduct.induction_on with + | C1 => simp + | Cp h1 h2 => simp [map_add, h1, h2] lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · simp - · simp only [map_add, LinearMap.add_apply, hx₁, hx₂] + induction x using PiTensorProduct.induction_on with + | C1 => simp + | Cp h1 h2 => simp [h1, h2] instance nonAssocSemiring : NonAssocSemiring (⨂[R] i, A i) where __ := nonUnitalNonAssocSemiring @@ -117,16 +117,21 @@ variable [CommSemiring R] [∀ i, NonUnitalSemiring (A i)] variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · induction' z using PiTensorProduct.induction_on with rz z z₁ z₂ hz₁ hz₂ - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, mul_assoc] - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz₁ hz₂ ⊢ - rw [hz₁, hz₂] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] + induction x using PiTensorProduct.induction_on with -- rx x x₁ x₂ hx₁ hx₂ + | C1 => + induction y using PiTensorProduct.induction_on with + | C1 => + induction z using PiTensorProduct.induction_on with + | C1 => simp [mul_assoc] + | Cp hz1 hz2 => + simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz1 hz2 ⊢ + rw [hz1, hz2] + | Cp hy1 hy2 => + simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy1 hy2 ⊢ + rw [hy1, hy2] + | Cp hx1 hx2 => + simp only [map_add, LinearMap.add_apply] at hx1 hx2 ⊢ + rw [hx1, hx2] instance nonUnitalSemiring : NonUnitalSemiring (⨂[R] i, A i) where __ := nonUnitalNonAssocSemiring @@ -174,7 +179,7 @@ lemma algebraMap_apply (r : R) (i : ι) [DecidableEq ι] : congr /-- -the map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` +The map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` -/ @[simps] def fromComponentAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where @@ -198,14 +203,18 @@ def liftAlgHom {S : Type*} [Semiring S] [Algebra R S] toFun := lift f map_one' := show lift f (tprod R 1) = 1 by simp [one] map_mul' x y := show lift f (x * y) = lift f x * lift f y by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, tprod_mul_tprod, map_smul, + induction x using PiTensorProduct.induction_on with + | C1 => + induction y using PiTensorProduct.induction_on with + | C1 => + simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, tprod_mul_tprod, map_smul, lift.tprod, mul] - · simp only [Algebra.smul_mul_assoc, map_smul, lift.tprod, map_add] at hy₁ hy₂ ⊢ - rw [mul_add, map_add, smul_add, hy₁, hy₂, mul_add, smul_add] - · simp only [map_add] at hx₁ hx₂ ⊢ - rw [add_mul, map_add, hx₁, hx₂, add_mul] + | Cp hy1 hy2 => + simp only [Algebra.smul_mul_assoc, map_smul, lift.tprod, map_add] at hy1 hy2 ⊢ + rw [mul_add, map_add, smul_add, hy1, hy2, mul_add, smul_add] + | Cp hx1 hx2 => + simp only [map_add] at hx1 hx2 ⊢ + rw [add_mul, map_add, hx1, hx2, add_mul] map_zero' := by simp only [map_zero] map_add' x y := by simp only [map_add] commutes' r := show lift f (r • tprod R 1) = _ by @@ -228,15 +237,19 @@ noncomputable section CommSemiring variable [CommSemiring R] [∀ i, CommSemiring (A i)] [∀ i, Algebra R (A i)] lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by - induction' x using PiTensorProduct.induction_on with rx x x₁ x₂ hx₁ hx₂ - · induction' y using PiTensorProduct.induction_on with ry y y₁ y₂ hy₁ hy₂ - · simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] + induction x using PiTensorProduct.induction_on with + | C1 => + induction y using PiTensorProduct.induction_on with + | C1 => + simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] rw [smul_comm, mul_comm] - · simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, - smul_add] at hy₁ hy₂ ⊢ - rw [hy₁, hy₂] - · simp only [map_add, LinearMap.add_apply] at hx₁ hx₂ ⊢ - rw [hx₁, hx₂] + | Cp hy1 hy2 => + simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, smul_add] at hy1 hy2 + ⊢ + rw [hy1, hy2] + | Cp hx1 hx2 => + simp only [map_add, LinearMap.add_apply] at hx1 hx2 ⊢ + rw [hx1, hx2] instance commSemiring : CommSemiring (⨂[R] i, A i) where __ := semiring From d4d9c863413a2d6f31a177cebbbb730a14778900 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 20 Feb 2024 14:31:57 +0000 Subject: [PATCH 45/60] long line --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 9082adb6dadba4..51e9fff00f468d 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -1041,8 +1041,8 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g · exact Function.apply_update c f i f₀ j /-- -Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module. Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and -`M'` respectively. +Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module. +Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and `M'` respectively. If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear map of multilinear map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` by `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. -/ From bcf2d0c503b7bf1f1c6bc8ff8b401bce58bda233 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 20 Feb 2024 14:33:35 +0000 Subject: [PATCH 46/60] add apply --- Mathlib/RingTheory/PiTensorProduct.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 47e1a635566c05..2295f06ac02e8e 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -47,9 +47,9 @@ The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = ( def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := PiTensorProduct.piTensorHomMap₂ <| tprod R fun _ ↦ LinearMap.mul _ _ -@[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : +@[simp] lemma lmul_apply_tprod_tprod (x y : (i : ι) → A i) : lmul (tprod R x) (tprod R y) = tprod R (x * y) := by - simp only [lmul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply'] + simp only [lmul, piTensorHomMap₂_apply_tprod_tprod_tprod, LinearMap.mul_apply'] rfl instance mul : Mul (⨂[R] i, A i) where @@ -59,13 +59,13 @@ lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl @[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : (tprod R x) * (tprod R y) = tprod R (x * y) := - lmul_tprod_tprod x y + lmul_apply_tprod_tprod x y lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by change lmul _ _ = _ rw [map_smul, map_smul, mul_comm r s, mul_smul] - simp only [LinearMap.smul_apply, lmul_tprod_tprod] + simp only [LinearMap.smul_apply, lmul_apply_tprod_tprod] lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by induction x using PiTensorProduct.induction_on <;> simp @@ -124,7 +124,7 @@ lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) induction z using PiTensorProduct.induction_on with | C1 => simp [mul_assoc] | Cp hz1 hz2 => - simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz1 hz2 ⊢ + simp only [map_smul, LinearMap.smul_apply, lmul_apply_tprod_tprod, map_add] at hz1 hz2 ⊢ rw [hz1, hz2] | Cp hy1 hy2 => simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy1 hy2 ⊢ @@ -241,7 +241,7 @@ lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by | C1 => induction y using PiTensorProduct.induction_on with | C1 => - simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] + simp only [map_smul, LinearMap.smul_apply, lmul_apply_tprod_tprod] rw [smul_comm, mul_comm] | Cp hy1 hy2 => simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, smul_add] at hy1 hy2 From c2680cd843edd34127e5799e6338e6bfd07865ac Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 20 Feb 2024 15:47:23 +0000 Subject: [PATCH 47/60] revert apply_ --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 8 ++++---- Mathlib/RingTheory/PiTensorProduct.lean | 12 ++++++------ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index c119f1577fed56..7c043550adda42 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -461,7 +461,7 @@ This is `TensorProduct.map` for an arbitrary family of modules. def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := lift <| (tprod R).compLinearMap f -@[simp] lemma map_apply_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) : +@[simp] lemma map_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) : map f (tprod R x) = tprod R fun i ↦ f i (x i) := lift.tprod _ @@ -479,7 +479,7 @@ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) → map_add' _ _ := by ext; simp map_smul' _ _ := by ext; simp -@[simp] lemma piTensorHomMap_apply_tprod_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) : +@[simp] lemma piTensorHomMap_tprod_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) : piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [piTensorHomMap] @@ -493,7 +493,7 @@ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:= lift <| LinearMap.compMultilinearMap piTensorHomMap <| (tprod R).compLinearMap f -lemma map₂_apply_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : Π i, s i) (y : Π i, t i) : +lemma map₂_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : Π i, s i) (y : Π i, t i) : map₂ f (tprod R x) (tprod R y) = tprod R fun i ↦ f i (x i) (y i) := by simp [map₂] @@ -511,7 +511,7 @@ def piTensorHomMap₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] map_add' x y := by dsimp; ext; simp map_smul' r x := by dsimp; ext; simp -@[simp] lemma piTensorHomMap₂_apply_tprod_tprod_tprod +@[simp] lemma piTensorHomMap₂_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) : piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by simp [piTensorHomMap₂] diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 2295f06ac02e8e..47e1a635566c05 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -47,9 +47,9 @@ The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = ( def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := PiTensorProduct.piTensorHomMap₂ <| tprod R fun _ ↦ LinearMap.mul _ _ -@[simp] lemma lmul_apply_tprod_tprod (x y : (i : ι) → A i) : +@[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : lmul (tprod R x) (tprod R y) = tprod R (x * y) := by - simp only [lmul, piTensorHomMap₂_apply_tprod_tprod_tprod, LinearMap.mul_apply'] + simp only [lmul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply'] rfl instance mul : Mul (⨂[R] i, A i) where @@ -59,13 +59,13 @@ lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl @[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : (tprod R x) * (tprod R y) = tprod R (x * y) := - lmul_apply_tprod_tprod x y + lmul_tprod_tprod x y lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by change lmul _ _ = _ rw [map_smul, map_smul, mul_comm r s, mul_smul] - simp only [LinearMap.smul_apply, lmul_apply_tprod_tprod] + simp only [LinearMap.smul_apply, lmul_tprod_tprod] lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by induction x using PiTensorProduct.induction_on <;> simp @@ -124,7 +124,7 @@ lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) induction z using PiTensorProduct.induction_on with | C1 => simp [mul_assoc] | Cp hz1 hz2 => - simp only [map_smul, LinearMap.smul_apply, lmul_apply_tprod_tprod, map_add] at hz1 hz2 ⊢ + simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz1 hz2 ⊢ rw [hz1, hz2] | Cp hy1 hy2 => simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy1 hy2 ⊢ @@ -241,7 +241,7 @@ lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by | C1 => induction y using PiTensorProduct.induction_on with | C1 => - simp only [map_smul, LinearMap.smul_apply, lmul_apply_tprod_tprod] + simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] rw [smul_comm, mul_comm] | Cp hy1 hy2 => simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, smul_add] at hy1 hy2 From 8487d12f4b4508bfda683bbd397a67411c246152 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 23 Feb 2024 23:00:50 +0000 Subject: [PATCH 48/60] golf --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 7c043550adda42..3e7d0f5cf53631 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -474,10 +474,8 @@ This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules. Note that `PiTensorProduct.piTensorHomMap (tprod R f)` is equal to `PiTensorProduct.map f`. -/ -def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i where - toFun φ := lift <| lift (MultilinearMap.piLinearMap <| tprod R) φ - map_add' _ _ := by ext; simp - map_smul' _ _ := by ext; simp +def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i := + lift.toLinearMap ∘ₗ lift (MultilinearMap.piLinearMap <| tprod R) @[simp] lemma piTensorHomMap_tprod_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) : piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by From 9aa02c41fe97503b82743fc933dcac6142a5db61 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 23 Feb 2024 23:29:31 +0000 Subject: [PATCH 49/60] fix instance names --- Mathlib/RingTheory/PiTensorProduct.lean | 40 ++++++++++++------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 47e1a635566c05..f45b63b0b4db5f 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -26,12 +26,12 @@ noncomputable section AddCommMonoidWithOne variable [CommSemiring R] [∀ i, AddCommMonoidWithOne (A i)] [∀ i, Module R (A i)] -instance one : One (⨂[R] i, A i) where +instance instOne : One (⨂[R] i, A i) where one := tprod R 1 -instance addCommMonoidWithOne : AddCommMonoidWithOne (⨂[R] i, A i) where +instance instAddCommMonoidWithOne : AddCommMonoidWithOne (⨂[R] i, A i) where __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i)) - __ := one + __ := instOne end AddCommMonoidWithOne @@ -52,7 +52,7 @@ def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) : simp only [lmul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply'] rfl -instance mul : Mul (⨂[R] i, A i) where +instance instMul : Mul (⨂[R] i, A i) where mul x y := lmul x y lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl @@ -79,8 +79,8 @@ lemma lmul_add (x y z : ⨂[R] i, A i) : lmul x (y + z) = lmul x y + lmul x z := lemma add_lmul (x y z : ⨂[R] i, A i) : lmul (x + y) z = lmul x z + lmul y z := by induction x using PiTensorProduct.induction_on <;> simp -instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (⨂[R] i, A i) where - __ := mul +instance instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (⨂[R] i, A i) where + __ := instMul __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i)) left_distrib := lmul_add right_distrib := add_lmul @@ -104,8 +104,8 @@ lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by | C1 => simp | Cp h1 h2 => simp [h1, h2] -instance nonAssocSemiring : NonAssocSemiring (⨂[R] i, A i) where - __ := nonUnitalNonAssocSemiring +instance instNonAssocSemiring : NonAssocSemiring (⨂[R] i, A i) where + __ := instNonUnitalNonAssocSemiring one_mul := one_lmul mul_one := lmul_one @@ -133,8 +133,8 @@ lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) simp only [map_add, LinearMap.add_apply] at hx1 hx2 ⊢ rw [hx1, hx2] -instance nonUnitalSemiring : NonUnitalSemiring (⨂[R] i, A i) where - __ := nonUnitalNonAssocSemiring +instance instNonUnitalSemiring : NonUnitalSemiring (⨂[R] i, A i) where + __ := instNonUnitalNonAssocSemiring mul_assoc := lmul_assoc end NonUnitalSemiring @@ -143,11 +143,11 @@ noncomputable section Semiring variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] -instance semiring : Semiring (⨂[R] i, A i) where - __ := nonUnitalSemiring - __ := nonAssocSemiring +instance instSemiring : Semiring (⨂[R] i, A i) where + __ := instNonUnitalSemiring + __ := instNonAssocSemiring -instance algebra : Algebra R (⨂[R] i, A i) where +instance instAlgebra : Algebra R (⨂[R] i, A i) where __ := hasSMul' toFun := (· • 1) map_one' := by simp @@ -226,8 +226,8 @@ noncomputable section Ring variable [CommRing R] [∀ i, Ring (A i)] [∀ i, Algebra R (A i)] -instance ring : Ring (⨂[R] i, A i) where - __ := semiring +instance instRing : Ring (⨂[R] i, A i) where + __ := instSemiring __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) end Ring @@ -251,8 +251,8 @@ lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by simp only [map_add, LinearMap.add_apply] at hx1 hx2 ⊢ rw [hx1, hx2] -instance commSemiring : CommSemiring (⨂[R] i, A i) where - __ := semiring +instance instCommSemiring : CommSemiring (⨂[R] i, A i) where + __ := instSemiring __ := inferInstanceAs <| AddCommMonoid (⨂[R] i, A i) mul_comm := lmul_comm @@ -261,8 +261,8 @@ end CommSemiring noncomputable section CommRing variable [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] -instance commRing : CommRing (⨂[R] i, A i) where - __ := commSemiring +instance instCommRing : CommRing (⨂[R] i, A i) where + __ := instCommSemiring __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i) end CommRing From fea8428a42db88025a9bb8ac1381bffb005e6615 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 23 Feb 2024 23:33:48 +0000 Subject: [PATCH 50/60] golf some proofs, rename lmul to mul to match RingTheory/TensorProduct --- Mathlib/RingTheory/PiTensorProduct.lean | 104 +++++++++--------------- 1 file changed, 38 insertions(+), 66 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index f45b63b0b4db5f..dc05fd14525d11 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -44,48 +44,36 @@ attribute [aesop safe] mul_add mul_smul_comm smul_mul_assoc add_mul in /-- The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)` -/ -def lmul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := +def mul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) := PiTensorProduct.piTensorHomMap₂ <| tprod R fun _ ↦ LinearMap.mul _ _ -@[simp] lemma lmul_tprod_tprod (x y : (i : ι) → A i) : - lmul (tprod R x) (tprod R y) = tprod R (x * y) := by - simp only [lmul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply'] +@[simp] lemma mul_tprod_tprod (x y : (i : ι) → A i) : + mul (tprod R x) (tprod R y) = tprod R (x * y) := by + simp only [mul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply'] rfl instance instMul : Mul (⨂[R] i, A i) where - mul x y := lmul x y + mul x y := mul x y -lemma mul_def (x y : ⨂[R] i, A i) : x * y = lmul x y := rfl +lemma mul_def (x y : ⨂[R] i, A i) : x * y = mul x y := rfl @[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) : - (tprod R x) * (tprod R y) = tprod R (x * y) := - lmul_tprod_tprod x y + tprod R x * tprod R y = tprod R (x * y) := + mul_tprod_tprod x y lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) : - (r • tprod R x) * (s • tprod R y) = (r * s) • (tprod R (x * y)) := by - change lmul _ _ = _ + (r • tprod R x) * (s • tprod R y) = (r * s) • tprod R (x * y) := by + change mul _ _ = _ rw [map_smul, map_smul, mul_comm r s, mul_smul] - simp only [LinearMap.smul_apply, lmul_tprod_tprod] - -lemma zero_lmul (x : ⨂[R] i, A i) : lmul 0 x = 0 := by - induction x using PiTensorProduct.induction_on <;> simp - -lemma lmul_zero (x : ⨂[R] i, A i) : lmul x 0 = 0 := by - induction x using PiTensorProduct.induction_on <;> simp - -lemma lmul_add (x y z : ⨂[R] i, A i) : lmul x (y + z) = lmul x y + lmul x z := by - induction x using PiTensorProduct.induction_on <;> simp - -lemma add_lmul (x y z : ⨂[R] i, A i) : lmul (x + y) z = lmul x z + lmul y z := by - induction x using PiTensorProduct.induction_on <;> simp + simp only [LinearMap.smul_apply, mul_tprod_tprod] instance instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (⨂[R] i, A i) where __ := instMul __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i)) - left_distrib := lmul_add - right_distrib := add_lmul - zero_mul := zero_lmul - mul_zero := lmul_zero + left_distrib _ _ _ := (mul _).map_add _ _ + right_distrib _ _ _ := mul.map_add₂ _ _ _ + zero_mul _ := mul.map_zero₂ _ + mul_zero _ := map_zero (mul _) end NonUnitalNonAssocSemiring @@ -94,20 +82,20 @@ noncomputable section NonAssocSemiring variable [CommSemiring R] [∀ i, NonAssocSemiring (A i)] variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] -lemma one_lmul (x : ⨂[R] i, A i) : lmul (tprod R 1) x = x := by +protected lemma one_mul (x : ⨂[R] i, A i) : mul (tprod R 1) x = x := by induction x using PiTensorProduct.induction_on with | C1 => simp | Cp h1 h2 => simp [map_add, h1, h2] -lemma lmul_one (x : ⨂[R] i, A i) : lmul x (tprod R 1) = x := by +protected lemma mul_one (x : ⨂[R] i, A i) : mul x (tprod R 1) = x := by induction x using PiTensorProduct.induction_on with | C1 => simp | Cp h1 h2 => simp [h1, h2] instance instNonAssocSemiring : NonAssocSemiring (⨂[R] i, A i) where __ := instNonUnitalNonAssocSemiring - one_mul := one_lmul - mul_one := lmul_one + one_mul := PiTensorProduct.one_mul + mul_one := PiTensorProduct.mul_one end NonAssocSemiring @@ -116,26 +104,18 @@ noncomputable section NonUnitalSemiring variable [CommSemiring R] [∀ i, NonUnitalSemiring (A i)] variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)] -lemma lmul_assoc (x y z : ⨂[R] i, A i) : lmul (lmul x y) z = lmul x (lmul y z) := by - induction x using PiTensorProduct.induction_on with -- rx x x₁ x₂ hx₁ hx₂ - | C1 => - induction y using PiTensorProduct.induction_on with - | C1 => - induction z using PiTensorProduct.induction_on with - | C1 => simp [mul_assoc] - | Cp hz1 hz2 => - simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod, map_add] at hz1 hz2 ⊢ - rw [hz1, hz2] - | Cp hy1 hy2 => - simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply] at hy1 hy2 ⊢ - rw [hy1, hy2] - | Cp hx1 hx2 => - simp only [map_add, LinearMap.add_apply] at hx1 hx2 ⊢ - rw [hx1, hx2] +protected lemma mul_assoc (x y z : ⨂[R] i, A i) : mul (mul x y) z = mul x (mul y z) := by + -- restate as an equality of morphisms so that we can use `ext` + suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul = + (LinearMap.llcomp R _ _ _ LinearMap.lflip <| LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by + exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z + ext x y z + dsimp [←mul_def] + simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z) instance instNonUnitalSemiring : NonUnitalSemiring (⨂[R] i, A i) where __ := instNonUnitalNonAssocSemiring - mul_assoc := lmul_assoc + mul_assoc := PiTensorProduct.mul_assoc end NonUnitalSemiring @@ -151,7 +131,7 @@ instance instAlgebra : Algebra R (⨂[R] i, A i) where __ := hasSMul' toFun := (· • 1) map_one' := by simp - map_mul' r s :=show (r * s) • 1 = lmul (r • 1) (s • 1) by + map_mul' r s :=show (r * s) • 1 = mul (r • 1) (s • 1) by rw [map_smul, map_smul, LinearMap.smul_apply, mul_comm, mul_smul] congr show (1 : ⨂[R] i, A i) = 1 * 1 @@ -160,13 +140,13 @@ instance instAlgebra : Algebra R (⨂[R] i, A i) where map_add' := by simp [add_smul] commutes' r x := by simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] - change lmul _ _ = lmul _ _ + change mul _ _ = mul _ _ rw [map_smul, map_smul, LinearMap.smul_apply] change r • (1 * x) = r • (x * 1) rw [mul_one, one_mul] smul_def' r x := by simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] - change _ = lmul _ _ + change _ = mul _ _ rw [map_smul, LinearMap.smul_apply] change _ = r • (1 * x) rw [one_mul] @@ -236,25 +216,17 @@ noncomputable section CommSemiring variable [CommSemiring R] [∀ i, CommSemiring (A i)] [∀ i, Algebra R (A i)] -lemma lmul_comm (x y : ⨂[R] i, A i) : lmul x y = lmul y x := by - induction x using PiTensorProduct.induction_on with - | C1 => - induction y using PiTensorProduct.induction_on with - | C1 => - simp only [map_smul, LinearMap.smul_apply, lmul_tprod_tprod] - rw [smul_comm, mul_comm] - | Cp hy1 hy2 => - simp only [map_smul, LinearMap.smul_apply, map_add, LinearMap.add_apply, smul_add] at hy1 hy2 - ⊢ - rw [hy1, hy2] - | Cp hx1 hx2 => - simp only [map_add, LinearMap.add_apply] at hx1 hx2 ⊢ - rw [hx1, hx2] +protected lemma mul_comm (x y : ⨂[R] i, A i) : mul x y = mul y x := by + suffices mul (R := R) (A := A) = mul.flip from + DFunLike.congr_fun (DFunLike.congr_fun this x) y + ext x y + dsimp + simp only [mul_tprod_tprod, mul_tprod_tprod, mul_comm x y] instance instCommSemiring : CommSemiring (⨂[R] i, A i) where __ := instSemiring __ := inferInstanceAs <| AddCommMonoid (⨂[R] i, A i) - mul_comm := lmul_comm + mul_comm := PiTensorProduct.mul_comm end CommSemiring From 1d7b385dffadbdee0e4384e46f8d63bbd6568a98 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 23 Feb 2024 23:38:58 +0000 Subject: [PATCH 51/60] helper lemmas --- Mathlib/RingTheory/PiTensorProduct.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index dc05fd14525d11..872a6f874b7ace 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -6,6 +6,7 @@ Authors: Jujian Zhang import Mathlib.LinearAlgebra.PiTensorProduct import Mathlib.Algebra.Algebra.Bilinear +import Mathlib.Algebra.Algebra.Pi /-! # Tensor product of `R`-algebras and rings @@ -29,6 +30,8 @@ variable [CommSemiring R] [∀ i, AddCommMonoidWithOne (A i)] [∀ i, Module R ( instance instOne : One (⨂[R] i, A i) where one := tprod R 1 +lemma one_def : 1 = tprod R (1 : Π i, A i) := rfl + instance instAddCommMonoidWithOne : AddCommMonoidWithOne (⨂[R] i, A i) where __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i)) __ := instOne From 1df8f62d34ffd474ddb0edc7cfe155d0e06189d5 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 24 Feb 2024 00:03:48 +0000 Subject: [PATCH 52/60] towers of algebras --- Mathlib/RingTheory/PiTensorProduct.lean | 26 ++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 872a6f874b7ace..59775f12a842a9 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -19,7 +19,7 @@ In particular if we take `R` to be `ℤ`, then this collapse into tensor product open TensorProduct Function -variable {ι R : Type*} {A : ι → Type*} +variable {ι R' R : Type*} {A : ι → Type*} namespace PiTensorProduct @@ -124,18 +124,21 @@ end NonUnitalSemiring noncomputable section Semiring -variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] +variable [CommSemiring R'] [CommSemiring R] [∀ i, Semiring (A i)] +variable [Algebra R' R] [∀ i, Algebra R (A i)] [∀ i, Algebra R' (A i)] +variable [∀ i, IsScalarTower R' R (A i)] instance instSemiring : Semiring (⨂[R] i, A i) where __ := instNonUnitalSemiring __ := instNonAssocSemiring -instance instAlgebra : Algebra R (⨂[R] i, A i) where +instance instAlgebra : Algebra R' (⨂[R] i, A i) where __ := hasSMul' toFun := (· • 1) map_one' := by simp - map_mul' r s :=show (r * s) • 1 = mul (r • 1) (s • 1) by - rw [map_smul, map_smul, LinearMap.smul_apply, mul_comm, mul_smul] + map_mul' r s := show (r * s) • 1 = mul (r • 1) (s • 1) by + rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply, mul_comm, + mul_smul] congr show (1 : ⨂[R] i, A i) = 1 * 1 rw [mul_one] @@ -144,21 +147,22 @@ instance instAlgebra : Algebra R (⨂[R] i, A i) where commutes' r x := by simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] change mul _ _ = mul _ _ - rw [map_smul, map_smul, LinearMap.smul_apply] + rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply] change r • (1 * x) = r • (x * 1) rw [mul_one, one_mul] smul_def' r x := by simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] change _ = mul _ _ - rw [map_smul, LinearMap.smul_apply] + rw [LinearMap.map_smul_of_tower, LinearMap.smul_apply] change _ = r • (1 * x) rw [one_mul] -lemma algebraMap_apply (r : R) (i : ι) [DecidableEq ι] : - algebraMap R (⨂[R] i, A i) r = tprod R (Pi.mulSingle i (algebraMap R (A i) r)) := by +lemma algebraMap_apply (r : R') (i : ι) [DecidableEq ι] : + algebraMap R' (⨂[R] i, A i) r = tprod R (Pi.mulSingle i (algebraMap R' (A i) r)) := by change r • tprod R 1 = _ - rw [show Pi.mulSingle i (algebraMap R (A i) r) = update (fun i ↦ 1) i (r • 1) by - · rw [Algebra.algebraMap_eq_smul_one]; rfl, MultilinearMap.map_smul, update_eq_self] + have : Pi.mulSingle i (algebraMap R' (A i) r) = update (fun i ↦ 1) i (r • 1) := by + rw [Algebra.algebraMap_eq_smul_one]; rfl + rw [this, ←smul_one_smul R r (1 : A i), MultilinearMap.map_smul, update_eq_self, smul_one_smul] congr /-- From e060c87135139285efa239b347f290f660ed3e6e Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 26 Feb 2024 10:47:21 +0000 Subject: [PATCH 53/60] Apply suggestions from code review Co-authored-by: Riccardo Brasca Co-authored-by: Eric Wieser Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- Mathlib/LinearAlgebra/PiTensorProduct.lean | 7 ++++--- Mathlib/RingTheory/PiTensorProduct.lean | 9 ++++----- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 51e9fff00f468d..802e73874a703a 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -1044,7 +1044,7 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module. Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and `M'` respectively. If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear -map of multilinear map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` by `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. +map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` via `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`. -/ @[simps!] def piLinearMap : MultilinearMap R M₁' M₂ →ₗ[R] diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 3e7d0f5cf53631..45819a3c2887b3 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -467,7 +467,7 @@ def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i /-- Let `sᵢ` and `tᵢ` be families of `R`-modules. -Then there is an `R`=linear map between `⨂ᵢ Hom(sᵢ, tᵢ)` and `Hom(⨂ᵢ sᵢ, ⨂ tᵢ)` defined by +Then there is an `R`-linear map between `⨂ᵢ Hom(sᵢ, tᵢ)` and `Hom(⨂ᵢ sᵢ, ⨂ tᵢ)` defined by `⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ fᵢ aᵢ`. This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules. @@ -482,10 +482,11 @@ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) → simp [piTensorHomMap] /-- -Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, i.e. `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an +Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, then `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`. -This is `TensorProduct.map` for two arbitrary families of modules. +This is `PiTensorProduct.map` for two arbitrary families of modules. +Note that for now, there is no `TensorProduct` analogue of this construction. -/ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:= diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 59775f12a842a9..12e7991ffdaf6e 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -11,10 +11,9 @@ import Mathlib.Algebra.Algebra.Pi /-! # Tensor product of `R`-algebras and rings -If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor `⨂ᵢ Aᵢ` is an `R`-algebra as well with -its structure map defined by `r ↦ r • 1`. +If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor product `⨂ᵢ Aᵢ` is an `R`-algebra as well with structure map defined by `r ↦ r • 1`. -In particular if we take `R` to be `ℤ`, then this collapse into tensor product of rings. +In particular if we take `R` to be `ℤ`, then this collapses into the tensor product of rings. -/ open TensorProduct Function @@ -113,7 +112,7 @@ protected lemma mul_assoc (x y z : ⨂[R] i, A i) : mul (mul x y) z = mul x (mul (LinearMap.llcomp R _ _ _ LinearMap.lflip <| LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z ext x y z - dsimp [←mul_def] + dsimp [← mul_def] simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z) instance instNonUnitalSemiring : NonUnitalSemiring (⨂[R] i, A i) where @@ -162,7 +161,7 @@ lemma algebraMap_apply (r : R') (i : ι) [DecidableEq ι] : change r • tprod R 1 = _ have : Pi.mulSingle i (algebraMap R' (A i) r) = update (fun i ↦ 1) i (r • 1) := by rw [Algebra.algebraMap_eq_smul_one]; rfl - rw [this, ←smul_one_smul R r (1 : A i), MultilinearMap.map_smul, update_eq_self, smul_one_smul] + rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_smul, update_eq_self, smul_one_smul] congr /-- From ddf6a5a57f20449bd18fd8a868a487a9b65b6ebd Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 26 Feb 2024 10:59:29 +0000 Subject: [PATCH 54/60] fix --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 4 ++++ Mathlib/RingTheory/PiTensorProduct.lean | 16 ++++++++-------- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 34829a4973686a..e1315388652820 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -485,6 +485,10 @@ def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) → piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [piTensorHomMap] +lemma piTensorHomMap_tprod_eq_map (f : Π i, s i →ₗ[R] t i) : + piTensorHomMap (tprod R f) = map f := by + ext; simp + /-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, then `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`. diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 12e7991ffdaf6e..50a059a9e4abe9 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -86,13 +86,13 @@ variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, Is protected lemma one_mul (x : ⨂[R] i, A i) : mul (tprod R 1) x = x := by induction x using PiTensorProduct.induction_on with - | C1 => simp - | Cp h1 h2 => simp [map_add, h1, h2] + | smul_tprod => simp + | add _ _ h1 h2 => simp [map_add, h1, h2] protected lemma mul_one (x : ⨂[R] i, A i) : mul x (tprod R 1) = x := by induction x using PiTensorProduct.induction_on with - | C1 => simp - | Cp h1 h2 => simp [h1, h2] + | smul_tprod => simp + | add _ _ h1 h2 => simp [h1, h2] instance instNonAssocSemiring : NonAssocSemiring (⨂[R] i, A i) where __ := instNonUnitalNonAssocSemiring @@ -190,15 +190,15 @@ def liftAlgHom {S : Type*} [Semiring S] [Algebra R S] map_one' := show lift f (tprod R 1) = 1 by simp [one] map_mul' x y := show lift f (x * y) = lift f x * lift f y by induction x using PiTensorProduct.induction_on with - | C1 => + | smul_tprod => induction y using PiTensorProduct.induction_on with - | C1 => + | smul_tprod => simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, tprod_mul_tprod, map_smul, lift.tprod, mul] - | Cp hy1 hy2 => + | add _ _ hy1 hy2 => simp only [Algebra.smul_mul_assoc, map_smul, lift.tprod, map_add] at hy1 hy2 ⊢ rw [mul_add, map_add, smul_add, hy1, hy2, mul_add, smul_add] - | Cp hx1 hx2 => + | add _ _ hx1 hx2 => simp only [map_add] at hx1 hx2 ⊢ rw [add_mul, map_add, hx1, hx2, add_mul] map_zero' := by simp only [map_zero] From b2c500583fc17b49b8936fd3752d87d094a97701 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 26 Feb 2024 11:01:29 +0000 Subject: [PATCH 55/60] fix long line --- Mathlib/RingTheory/PiTensorProduct.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 50a059a9e4abe9..349e31cb4e42e2 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -11,7 +11,8 @@ import Mathlib.Algebra.Algebra.Pi /-! # Tensor product of `R`-algebras and rings -If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor product `⨂ᵢ Aᵢ` is an `R`-algebra as well with structure map defined by `r ↦ r • 1`. +If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor product `⨂ᵢ Aᵢ` is an `R`-algebra as well +with structure map defined by `r ↦ r • 1`. In particular if we take `R` to be `ℤ`, then this collapses into the tensor product of rings. -/ From d1f91b2de4be4e2c4a01f234d84d3e8337be1de2 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 26 Feb 2024 11:42:55 +0000 Subject: [PATCH 56/60] shake fix --- Mathlib/RingTheory/PiTensorProduct.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 349e31cb4e42e2..064edf8b310b5f 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -6,7 +6,6 @@ Authors: Jujian Zhang import Mathlib.LinearAlgebra.PiTensorProduct import Mathlib.Algebra.Algebra.Bilinear -import Mathlib.Algebra.Algebra.Pi /-! # Tensor product of `R`-algebras and rings From 0f9e789f7d9616cbb67ee2132f240df09cb73071 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 26 Feb 2024 15:38:53 +0000 Subject: [PATCH 57/60] Update PiTensorProduct.lean --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index e1315388652820..5e034e05e650b0 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -494,6 +494,7 @@ Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, then `f : Πᵢ sᵢ element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`. This is `PiTensorProduct.map` for two arbitrary families of modules. +This is `TensorProduct.map₂` for families of modules. Note that for now, there is no `TensorProduct` analogue of this construction. -/ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : From d126d3c0269a78e4dfd64e499d444bad5a2ecb75 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 28 Feb 2024 22:25:09 +0000 Subject: [PATCH 58/60] Update Mathlib/RingTheory/PiTensorProduct.lean Co-authored-by: Eric Wieser --- Mathlib/RingTheory/PiTensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 064edf8b310b5f..0ddafeb090bcf9 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -168,7 +168,7 @@ lemma algebraMap_apply (r : R') (i : ι) [DecidableEq ι] : The map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...` -/ @[simps] -def fromComponentAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where +def singleAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where toFun a := tprod R (MonoidHom.single _ i a) map_one' := by simp only [_root_.map_one]; rfl map_mul' a a' := by simp From de2cf4822d8c16cc2edffaa6f53bfba3faa14bf2 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 28 Feb 2024 22:30:38 +0000 Subject: [PATCH 59/60] apply suggestions from code review --- Mathlib/RingTheory/PiTensorProduct.lean | 25 ++++--------------------- 1 file changed, 4 insertions(+), 21 deletions(-) diff --git a/Mathlib/RingTheory/PiTensorProduct.lean b/Mathlib/RingTheory/PiTensorProduct.lean index 0ddafeb090bcf9..c845711e5aa070 100644 --- a/Mathlib/RingTheory/PiTensorProduct.lean +++ b/Mathlib/RingTheory/PiTensorProduct.lean @@ -182,29 +182,12 @@ def singleAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where /-- Lifting a multilinear map to an algebra homomorphism from tensor product -/ -@[simps] +@[simps!] def liftAlgHom {S : Type*} [Semiring S] [Algebra R S] (f : MultilinearMap R A S) - (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : (⨂[R] i, A i) →ₐ[R] S where - toFun := lift f - map_one' := show lift f (tprod R 1) = 1 by simp [one] - map_mul' x y := show lift f (x * y) = lift f x * lift f y by - induction x using PiTensorProduct.induction_on with - | smul_tprod => - induction y using PiTensorProduct.induction_on with - | smul_tprod => - simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, tprod_mul_tprod, map_smul, - lift.tprod, mul] - | add _ _ hy1 hy2 => - simp only [Algebra.smul_mul_assoc, map_smul, lift.tprod, map_add] at hy1 hy2 ⊢ - rw [mul_add, map_add, smul_add, hy1, hy2, mul_add, smul_add] - | add _ _ hx1 hx2 => - simp only [map_add] at hx1 hx2 ⊢ - rw [add_mul, map_add, hx1, hx2, add_mul] - map_zero' := by simp only [map_zero] - map_add' x y := by simp only [map_add] - commutes' r := show lift f (r • tprod R 1) = _ by - rw [map_smul, lift.tprod, one, Algebra.algebraMap_eq_smul_one] + (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : (⨂[R] i, A i) →ₐ[R] S := + AlgHom.ofLinearMap (lift f) (show lift f (tprod R 1) = 1 by simp [one]) <| + LinearMap.map_mul_iff _ |>.mpr <| by aesop end Semiring From 57a624a449729622721a56f5e21202a9be769bda Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 28 Feb 2024 23:36:41 +0000 Subject: [PATCH 60/60] Update Mathlib/LinearAlgebra/PiTensorProduct.lean Co-authored-by: Eric Wieser --- Mathlib/LinearAlgebra/PiTensorProduct.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index 5e034e05e650b0..a708724a034dd8 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -495,7 +495,6 @@ element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ a This is `PiTensorProduct.map` for two arbitrary families of modules. This is `TensorProduct.map₂` for families of modules. -Note that for now, there is no `TensorProduct` analogue of this construction. -/ def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:=