From 80a505f6a533d327c3f8bffadf511660a4be953d Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 23 Oct 2024 07:27:45 +0000 Subject: [PATCH] feat: generalize Algebra.TensorProduct.rightAlgebra (#18089) Co-authored-by: Kevin Buzzard --- Mathlib/RingTheory/TensorProduct/Basic.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean index cbcde91fc95fd..dbb11acf62992 100644 --- a/Mathlib/RingTheory/TensorProduct/Basic.lean +++ b/Mathlib/RingTheory/TensorProduct/Basic.lean @@ -576,12 +576,22 @@ instance instCommRing : CommRing (A ⊗[R] B) := { toRing := inferInstance mul_comm := mul_comm } +end CommRing + section RightAlgebra +variable [CommSemiring R] +variable [Semiring A] [Algebra R A] +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) := - (Algebra.TensorProduct.includeRight.toRingHom : B →+* A ⊗[R] B).toAlgebra + 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] attribute [local instance] TensorProduct.rightAlgebra @@ -590,8 +600,6 @@ instance right_isScalarTower : IsScalarTower R B (A ⊗[R] B) := end RightAlgebra -end CommRing - /-- Verify that typeclass search finds the ring structure on `A ⊗[ℤ] B` when `A` and `B` are merely rings, by treating both as `ℤ`-algebras. -/