@[simp]

theorem Algebra.TensorProduct.map_comp_includeLeftRingHom {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : (↑(map f g)).comp includeLeftRingHom = includeLeftRingHom.comp ↑f

@[simp]

theorem Algebra.TensorProduct.rid_comp_includeLeftRingHom {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] : (↑(TensorProduct.rid R S A)).comp includeLeftRingHom = RingHom.id A

noncomputable def Algebra.TensorProduct.mapRingHom {R : Type u_1} {S : Type u_2} {T : Type u_3} {R' : Type u_4} {S' : Type u_5} {T' : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra R' T'] (fR : R →+* R') (fS : S →+* S') (fT : T →+* T') (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR) (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR) : TensorProduct R S T →+* TensorProduct R' S' T'

Heterobasic version of Algebra.TensorProduct.map as a ring homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.TensorProduct.mapRingHom_tmul {R : Type u_1} {S : Type u_2} {T : Type u_3} {R' : Type u_4} {S' : Type u_5} {T' : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra R' T'] (fR : R →+* R') (fS : S →+* S') (fT : T →+* T') (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR) (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR) (s : S) (t : T) : (mapRingHom fR fS fT HS HT) (s ⊗ₜ[R] t) = fS s ⊗ₜ[R'] fT t

@[simp]

theorem Algebra.TensorProduct.mapRingHom_comp_includeLeftRingHom {R : Type u_1} {S : Type u_2} {T : Type u_3} {R' : Type u_4} {S' : Type u_5} {T' : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra R' T'] (fR : R →+* R') (fS : S →+* S') (fT : T →+* T') (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR) (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR) : (mapRingHom fR fS fT HS HT).comp includeLeftRingHom = includeLeftRingHom.comp fS

@[simp]

theorem Algebra.TensorProduct.mapRingHom_comp_includeRight {R : Type u_1} {S : Type u_2} {T : Type u_3} {R' : Type u_4} {S' : Type u_5} {T' : Type u_6} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra R' T'] (fR : R →+* R') (fS : S →+* S') (fT : T →+* T') (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR) (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR) : (mapRingHom fR fS fT HS HT).comp ↑includeRight = (↑includeRight).comp fT