Skip to content

[Merged by Bors] - chore(RingTheory/TensorProduct): more product compatibilities #24380

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
chrisflav wants to merge 2 commits into from
Closed

[Merged by Bors] - chore(RingTheory/TensorProduct): more product compatibilities #24380

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ea4e1a7
tensorproduct binary prod
chrisflav Apr 26, 2025
0403590
review suggestions
chrisflav May 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 37 additions & 4 deletions Mathlib/RingTheory/TensorProduct/Pi.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Authors: Christian Merten
-/
import Mathlib.Algebra.Algebra.Pi
import Mathlib.LinearAlgebra.TensorProduct.Pi
import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.RingTheory.TensorProduct.Basic

/-!
Expand All @@ -17,7 +18,7 @@ is a direct application of `Mathlib.LinearAlgebra.TensorProduct.Pi` to the algeb

open TensorProduct

section
namespace Algebra.TensorProduct

variable (R S A : Type*) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A]
[Algebra R A] [Algebra S A] [IsScalarTower R S A]
Expand Down Expand Up @@ -47,12 +48,44 @@ noncomputable def piRightHom : A ⊗[R] (∀ i, B i) →ₐ[S] ∀ i, A ⊗[R] B
variable [Fintype ι] [DecidableEq ι]

/-- Tensor product of rings commutes with finite products on the right. -/
noncomputable def Algebra.TensorProduct.piRight :
A ⊗[R] (∀ i, B i) ≃ₐ[S] ∀ i, A ⊗[R] B i :=
noncomputable def piRight : A ⊗[R] (∀ i, B i) ≃ₐ[S] ∀ i, A ⊗[R] B i :=
AlgEquiv.ofLinearEquiv (_root_.TensorProduct.piRight R S A B) (by simp) (by simp)

@[simp]
lemma Algebra.TensorProduct.piRight_tmul (x : A) (f : ∀ i, B i) :
lemma piRight_tmul (x : A) (f : ∀ i, B i) :
piRight R S A B (x ⊗ₜ f) = (fun j ↦ x ⊗ₜ f j) := rfl

variable (ι) in
/-- Variant of `Algebra.TensorProduct.piRight` with constant factors. -/
noncomputable def piScalarRight : A ⊗[R] (ι → R) ≃ₐ[S] ι → A :=
(piRight R S A (fun _ : ι ↦ R)).trans <|
AlgEquiv.piCongrRight (fun _ ↦ Algebra.TensorProduct.rid R S A)

@[simp]
lemma piScalarRight_tmul (x : A) (y : ι → R) :
piScalarRight R S A ι (x ⊗ₜ y) = fun i ↦ y i • x :=
rfl

section

variable (B C : Type*) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C]

/-- Tensor product of rings commutes with binary products on the right. -/
noncomputable nonrec def prodRight : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C :=
AlgEquiv.ofLinearEquiv (TensorProduct.prodRight R S A B C)
(by simp [Algebra.TensorProduct.one_def])
(LinearMap.map_mul_of_map_mul_tmul (fun _ _ _ _ ↦ by simp))

@[simp]
lemma prodRight_tmul (a : A) (x : B × C) : prodRight R S A B C (a ⊗ₜ x) = (a ⊗ₜ x.1, a ⊗ₜ x.2) :=
rfl

@[simp]
lemma prodRight_symm_tmul (a : A) (b : B) (c : C) :
(prodRight R S A B C).symm (a ⊗ₜ b, a ⊗ₜ c) = a ⊗ₜ (b, c) := by
apply (prodRight R S A B C).injective
simp

end

end Algebra.TensorProduct
Loading