From ae676200bbb69d8cf4b7cbbb041c0c2a432dbb82 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 5 Jun 2025 12:23:11 +0100 Subject: [PATCH 1/5] chore: refactor Algebra.TensorProduct.rightAlgebra --- Mathlib/RingTheory/TensorProduct/Basic.lean | 33 +++++++++++++++++---- 1 file changed, 27 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean index 67716ee83b32c1..ba00fdbe9324bb 100644 --- a/Mathlib/RingTheory/TensorProduct/Basic.lean +++ b/Mathlib/RingTheory/TensorProduct/Basic.lean @@ -604,12 +604,33 @@ variable [CommSemiring B] [Algebra R B] /-- `S ⊗[R] T` has a `T`-algebra structure. This is not a global instance or else the action of `S` on `S ⊗[R] S` would be ambiguous. -/ -abbrev rightAlgebra : Algebra B (A ⊗[R] B) := - includeRight.toRingHom.toAlgebra' fun b x => by - suffices LinearMap.mulLeft R (includeRight b) = LinearMap.mulRight R (includeRight b) from - congr($this x) - ext xa xb - simp [mul_comm] +abbrev rightAlgebra : Algebra B (A ⊗[R] B) where + smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e)) + algebraMap := Algebra.TensorProduct.includeRight.toRingHom + commutes' s bs := by + induction bs with + | zero => simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + Algebra.TensorProduct.includeRight_apply, mul_zero, zero_mul] + | tmul x y => + simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, one_mul, + mul_one, mul_comm] + | add x y _ _ => + simp_all only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + Algebra.TensorProduct.includeRight_apply, mul_add, add_mul] + smul_def' s bs := by + induction bs with + | zero => simp; sorry + | tmul x y => + simp only [smul_def, TensorProduct.comm_tmul, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, one_mul] + sorry +-- rw [TensorProduct.smul_tmul'] +-- simp only [smul_eq_mul, TensorProduct.comm_symm_tmul] + | add x y hx hy => + simp_all only [smul_def, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + Algebra.TensorProduct.includeRight_apply, smul_add, ← hx, ← hy, mul_add] + sorry attribute [local instance] TensorProduct.rightAlgebra From 6985eadbc66a4ea2908e02d7f244a6fc64bf721e Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 5 Jun 2025 12:35:11 +0100 Subject: [PATCH 2/5] add helpful simp lemma --- Mathlib/RingTheory/TensorProduct/Basic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean index ba00fdbe9324bb..a15d3464a70240 100644 --- a/Mathlib/RingTheory/TensorProduct/Basic.lean +++ b/Mathlib/RingTheory/TensorProduct/Basic.lean @@ -605,7 +605,7 @@ variable [CommSemiring B] [Algebra R B] /-- `S ⊗[R] T` has a `T`-algebra structure. This is not a global instance or else the action of `S` on `S ⊗[R] S` would be ambiguous. -/ abbrev rightAlgebra : Algebra B (A ⊗[R] B) where - smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e)) + smul b ab := TensorProduct.comm _ _ _ (b • (TensorProduct.comm _ _ _ ab)) algebraMap := Algebra.TensorProduct.includeRight.toRingHom commutes' s bs := by induction bs with @@ -634,6 +634,8 @@ abbrev rightAlgebra : Algebra B (A ⊗[R] B) where attribute [local instance] TensorProduct.rightAlgebra +@[simp] lemma rightAlgebra.algebraMap_apply (b : B) : algebraMap B (A ⊗[R] B) b = 1 ⊗ₜ b := rfl + instance right_isScalarTower : IsScalarTower R B (A ⊗[R] B) := IsScalarTower.of_algebraMap_eq fun r => (Algebra.TensorProduct.includeRight.commutes r).symm From 68c2f244783f0fb54aa63811bf1a9c0f22e8154b Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 5 Jun 2025 12:42:09 +0100 Subject: [PATCH 3/5] linter hack --- Mathlib/RingTheory/TensorProduct/Basic.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean index a15d3464a70240..784fc2a4755757 100644 --- a/Mathlib/RingTheory/TensorProduct/Basic.lean +++ b/Mathlib/RingTheory/TensorProduct/Basic.lean @@ -34,6 +34,8 @@ multiplication is characterized by `(a₁ ⊗ₜ b₁) * (a₂ ⊗ₜ b₂) = (a -/ +set_option linter.style.longFile 1700 + assert_not_exists Equiv.Perm.cycleType suppress_compilation From 9e5325da8fcc7292ba12f57fd9ac0aca14d2dd71 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 5 Jun 2025 13:31:53 +0100 Subject: [PATCH 4/5] horrible proofs but does CI pass? --- Mathlib/RingTheory/TensorProduct/Basic.lean | 36 ++++++++++++++------- 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean index 784fc2a4755757..223f78cfe23d36 100644 --- a/Mathlib/RingTheory/TensorProduct/Basic.lean +++ b/Mathlib/RingTheory/TensorProduct/Basic.lean @@ -604,13 +604,23 @@ variable [CommSemiring R] variable [Semiring A] [Algebra R A] variable [CommSemiring B] [Algebra R B] +-- abbrev rightAlgebra.smul (b : B) (ab : A ⊗[R] B) : (A ⊗[R] B) := +-- TensorProduct.comm _ _ _ (b • (TensorProduct.comm _ _ _ ab)) + +-- @[simp] + +-- lemma smul_def (b : B) (ab : A ⊗[R] B) : +-- rightAlgebra.smul b ab = +-- (TensorProduct.comm _ _ _).symm (b • (TensorProduct.comm _ _ _ ab)) := rfl + + /-- `S ⊗[R] T` has a `T`-algebra structure. This is not a global instance or else the action of `S` on `S ⊗[R] S` would be ambiguous. -/ abbrev rightAlgebra : Algebra B (A ⊗[R] B) where smul b ab := TensorProduct.comm _ _ _ (b • (TensorProduct.comm _ _ _ ab)) algebraMap := Algebra.TensorProduct.includeRight.toRingHom - commutes' s bs := by - induction bs with + commutes' b ab := by + induction ab with | zero => simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply, mul_zero, zero_mul] | tmul x y => @@ -620,19 +630,21 @@ abbrev rightAlgebra : Algebra B (A ⊗[R] B) where | add x y _ _ => simp_all only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply, mul_add, add_mul] - smul_def' s bs := by - induction bs with - | zero => simp; sorry - | tmul x y => + smul_def' b ab := by + induction ab with + | zero => simp only [smul_zero, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + Algebra.TensorProduct.includeRight_apply, mul_zero]; rfl + | tmul a b => simp only [smul_def, TensorProduct.comm_tmul, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, one_mul] - sorry --- rw [TensorProduct.smul_tmul'] --- simp only [smul_eq_mul, TensorProduct.comm_symm_tmul] + simp only [HSMul.hSMul] + simp | add x y hx hy => - simp_all only [smul_def, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, - Algebra.TensorProduct.includeRight_apply, smul_add, ← hx, ← hy, mul_add] - sorry + change (TensorProduct.comm R B A) _ = _ + simp_all only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, includeRight_apply, map_add, + smul_add, mul_add] + rw [← hx, ← hy] + rfl attribute [local instance] TensorProduct.rightAlgebra From af78e117a468ff6847f600d66339e02ad5128edf Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 5 Jun 2025 14:38:06 +0100 Subject: [PATCH 5/5] tidy up proofs --- Mathlib/RingTheory/TensorProduct/Basic.lean | 32 +++++++-------------- 1 file changed, 11 insertions(+), 21 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean index 223f78cfe23d36..2364be9b05d58f 100644 --- a/Mathlib/RingTheory/TensorProduct/Basic.lean +++ b/Mathlib/RingTheory/TensorProduct/Basic.lean @@ -604,16 +604,6 @@ variable [CommSemiring R] variable [Semiring A] [Algebra R A] variable [CommSemiring B] [Algebra R B] --- abbrev rightAlgebra.smul (b : B) (ab : A ⊗[R] B) : (A ⊗[R] B) := --- TensorProduct.comm _ _ _ (b • (TensorProduct.comm _ _ _ ab)) - --- @[simp] - --- lemma smul_def (b : B) (ab : A ⊗[R] B) : --- rightAlgebra.smul b ab = --- (TensorProduct.comm _ _ _).symm (b • (TensorProduct.comm _ _ _ ab)) := rfl - - /-- `S ⊗[R] T` has a `T`-algebra structure. This is not a global instance or else the action of `S` on `S ⊗[R] S` would be ambiguous. -/ abbrev rightAlgebra : Algebra B (A ⊗[R] B) where @@ -632,19 +622,19 @@ abbrev rightAlgebra : Algebra B (A ⊗[R] B) where Algebra.TensorProduct.includeRight_apply, mul_add, add_mul] smul_def' b ab := by induction ab with - | zero => simp only [smul_zero, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, - Algebra.TensorProduct.includeRight_apply, mul_zero]; rfl + | zero => + change (TensorProduct.comm R B A) _ = _ + simp only [map_zero, smul_zero, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + includeRight_apply, mul_zero] | tmul a b => - simp only [smul_def, TensorProduct.comm_tmul, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, - Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, one_mul] - simp only [HSMul.hSMul] - simp - | add x y hx hy => change (TensorProduct.comm R B A) _ = _ - simp_all only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, includeRight_apply, map_add, - smul_add, mul_add] - rw [← hx, ← hy] - rfl + simp only [smul_def, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, + Algebra.TensorProduct.includeRight_apply, + algebraMap_apply, id.map_eq_id, RingHom.id_apply, comm_tmul, + tmul_mul_tmul] + | add x y hx hy => + change (TensorProduct.comm R B A) _ = _ at ⊢ hx hy + simp only [map_add, smul_add, mul_add, ← hx, ← hy] attribute [local instance] TensorProduct.rightAlgebra