Theorems · Definition · ring theory

Algebra.TensorProduct.mapRingHom

{R : Type u_3} →
  {S : Type u_4} →
    {T : Type u_5} →
      {R' : Type u_6} →
        {S' : Type u_7} →
          {T' : Type u_8} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring S] →
                [inst_2 : CommSemiring T] →
                  [inst_3 : Algebra R S] →
                    [inst_4 : Algebra R T] →
                      [inst_5 : CommSemiring R'] →
                        [inst_6 : CommSemiring S'] →
                          [inst_7 : CommSemiring T'] →
                            [inst_8 : Algebra R' S'] →
                              [inst_9 : Algebra R' T'] →
                                (fR : R →+* R') →
                                  (fS : S →+* S') →
                                    (fT : T →+* T') →
                                      fS.comp (algebraMap R S) = (algebraMap R' S').comp fR →
                                        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. Note that this would generalise map if we were to have SemiAlgHom.

Defined in

Mathlib.RingTheory.TensorProduct.Maps

Cited by

8 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringCommSemiringAlgebraAlgebraCommSemiringCommSemiringCommSemiringAlgebraAlgebra