Theorems · Definition · ring theory

Algebra.TensorProduct.liftEquiv

{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] →
                                    { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) } ≃
                                      (TensorProduct R A B →ₐ[S] C)

The universal property of the tensor product of algebras. Pairs of algebra morphisms that commute are equivalent to algebra morphisms from the tensor product. This is Algebra.TensorProduct.lift as an equivalence. See also GradedTensorProduct.liftEquiv for an alternative commutativity requirement for graded algebra.

Defined in

Mathlib.RingTheory.TensorProduct.Maps

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraSemiringAlgebraAlgebraIsScalarTowerSemiringAlgebraSemiringAlgebraAlgebraIsScalarTower