theorem FiberFunctorEnd.rTensor_lTensor_commute (k : Type u_1) [CommSemiring k] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] (φ : Module.End k M) (ψ : Module.End k N) : Commute ((Module.End.rTensorAlgHom k M N) φ) ((Module.End.lTensorAlgHom k N M) ψ)

Right-tensoring by φ : End M and left-tensoring by ψ : End N commute as endomorphisms of M ⊗ N.

def FiberFunctorEnd.endTensorEndAlgHom (k : Type u_1) [CommSemiring k] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] : TensorProduct k (Module.End k M) (Module.End k N) →ₐ[k] Module.End k (TensorProduct k M N)

The canonical k-algebra homomorphism End(M) ⊗ End(N) →ₐ End(M ⊗ N) obtained by combining right- and left-tensoring with the universal property of the algebra tensor product.

@[simp]

theorem FiberFunctorEnd.endTensorEndAlgHom_tmul (k : Type u_1) [CommSemiring k] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] (φ : Module.End k M) (ψ : Module.End k N) : (endTensorEndAlgHom k M N) (φ ⊗ₜ[k] ψ) = TensorProduct.map φ ψ

The algebra homomorphism endTensorEndAlgHom sends the elementary tensor φ ⊗ ψ to the endomorphism TensorProduct.map φ ψ of M ⊗ N.

noncomputable def FiberFunctorEnd.endTensorEndAlgEquiv (k : Type u_1) [CommSemiring k] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module.Free k M] [Module.Finite k M] [Module.Free k N] [Module.Finite k N] : TensorProduct k (Module.End k M) (Module.End k N) ≃ₐ[k] Module.End k (TensorProduct k M N)

For finite free k-modules M and N, the canonical algebra map upgrades to a k-algebra isomorphism End(M) ⊗ End(N) ≃ₐ End(M ⊗ N).

@[simp]

theorem FiberFunctorEnd.endTensorEndAlgEquiv_tmul (k : Type u_1) [CommSemiring k] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module.Free k M] [Module.Finite k M] [Module.Free k N] [Module.Finite k N] (φ : Module.End k M) (ψ : Module.End k N) : (endTensorEndAlgEquiv k M N) (φ ⊗ₜ[k] ψ) = TensorProduct.map φ ψ

The algebra isomorphism endTensorEndAlgEquiv sends φ ⊗ ψ to TensorProduct.map φ ψ.

noncomputable def FiberFunctorEnd.endTensorEndAlgEquiv_named (k : Type u_1) [CommSemiring k] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module.Free k M] [Module.Finite k M] [Module.Free k N] [Module.Finite k N] : TensorProduct k (Module.End k M) (Module.End k N) ≃ₐ[k] Module.End k (TensorProduct k M N)

Named alias of endTensorEndAlgEquiv, used as a downstream reference.