Theorems · Definition · ring theory

Algebra.TensorProduct.lift

{R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Semiring C] →
                              [inst_10 : Algebra S C] →
                                [inst_11 : Algebra R C] →
                                  [IsScalarTower R S C] →
                                    (f : A →ₐ[S] C) →
                                      (g : B →ₐ[R] C) →
                                        (∀ (x : A) (y : B), Commute (f x) (g y)) → TensorProduct R A B →ₐ[S] C

The forward direction of the universal property of tensor products of algebras; any algebra morphism from the tensor product can be factored as the product of two algebra morphisms that commute. See Algebra.TensorProduct.liftEquiv for the fact that every morphism factors this way.

Defined in

Mathlib.RingTheory.TensorProduct.Maps

Cited by

46 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraSemiringAlgebraAlgebraIsScalarTowerSemiringAlgebraSemiringAlgebraAlgebraIsScalarTower