TensorProduct of Endomorphism rings

Stream: Is there code for X?

[Edison Xie]

Do we have that for a commutative ring R, Module.End R (Fin n → R) ⊗[R] Module.End R (Fin m → R) ≃ₐ[R] Module.End R ((Fin n → R) ⊗[R] (Fin m → R))? I'm asking this because I'm trying to show tensor product of azumaya algebras is still azumaya.

[Edison Xie]

Moreover, do we have for finitely generated projective R-modules M and N, Module.End R M ⊗[R] Module.End R N ≃ₐ[R] Module.End R (M ⊗[R] N)?

[Eric Wieser]

@loogle TensorProduct _ (Module.End _ _) (Module.End _ _)

[loogle]

:search: Module.endTensorEndAlgHom, Module.endTensorEndAlgHom_apply

[Edison Xie]

hmmmm yeah that's the map

[Junyan Xu]

For free modules there is the LinearEquiv homTensorHomEquiv, which you can combine with the AlgHom to get the AlgEquiv. I'm about to generalize it to finite projective modules.

[Edison Xie]

I'm doing this generation right now :((