-
Notifications
You must be signed in to change notification settings - Fork 234
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.
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
[Merged by Bors] - feat(RingTheory/TensorProduct): the universal property of the tensor product of algebras #7409
Conversation
Rather than showing agreement on all the scalars, it suffices to show agreement on `1`.
…product of algebras
…fLinearMapTensorProduct
…sorProduct' into eric-wieser/TensorProduct.liftAlg
This PR/issue depends on: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we have the version in the commutative case? It follows from this one of course, but it is worth to have it without mention the commutator.
You're right, we did already have the commutative case (twice!). I've redefined it in terms of the non-commutative case. |
section | ||
|
||
variable [CommSemiring R] [CommSemiring S] [Algebra R S] | ||
variable [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] | ||
variable [Semiring B] [Algebra R B] | ||
variable [CommSemiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] | ||
|
||
/-- If `A`, `B`, `C` are `R`-algebras, `A` and `C` are also `S`-algebras (forming a tower as | ||
`·/S/R`), then the product map of `f : A →ₐ[S] C` and `g : B →ₐ[R] C` is an `S`-algebra | ||
homomorphism. | ||
|
||
This is just a special case of `Algebra.TensorProduct.lift` for when `C` is commutative. -/ | ||
abbrev productLeftAlgHom (f : A →ₐ[S] C) (g : B →ₐ[R] C) : A ⊗[R] B →ₐ[S] C := | ||
lift f g (fun _ _ => Commute.all _ _) | ||
#align algebra.tensor_product.product_left_alg_hom Algebra.TensorProduct.productLeftAlgHom | ||
|
||
end |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This was moved from further down the file, with its implementation replaced.
Thanks! bors merge |
…product of algebras (#7409) The construction used for `CliffordAlgebra.ofBaseChange` generalizes into a universal property for building arbitrary algebra morphisms out of the tensor product. It turns out this is a known result; it is mentioned at https://en.wikipedia.org/wiki/Tensor_product_of_algebras#Further_properties which cites the linked reference, though the version added by this PR is heterobasic like the rest of this file. This is a generalization of the existing `Algebra.TensorProduct.productLeftAlgHom` to non-commutative rings.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
The construction used for
CliffordAlgebra.ofBaseChange
generalizes into a universal property for building arbitrary algebra morphisms out of the tensor product.It turns out this is a known result; it is mentioned at https://en.wikipedia.org/wiki/Tensor_product_of_algebras#Further_properties which cites the linked reference, though the version added by this PR is heterobasic like the rest of this file.
This is a generalization of the existing
Algebra.TensorProduct.productLeftAlgHom
to non-commutative rings.