Theorems · Definition · commutative algebra

Algebra.TensorProduct.algEquivIncludeRange

(R : Type u_1) →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring T] →
              [inst_4 : Algebra R T] →
                TensorProduct R S T ≃ₐ[R]
                  TensorProduct R ↥Algebra.TensorProduct.includeLeft.range ↥Algebra.TensorProduct.includeRight.range

Given R-algebras S,T, there is a natural R-algebra isomorphism from S ⊗[R] T to S' ⊗[R] T' where S',T' are the images of S,T in S ⊗[R] T respectively.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Cited by

4 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringAlgebraSemiringAlgebra