Theorems · Definition · commutative algebra

Algebra.TensorProduct.linearEquivIncludeRange

(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-linear isomorphism from S ⊗[R] T to S' ⊗[R] T' where S',T' are the images of S,T in S ⊗[R] T respectively. This is promoted to an R-algebra isomorphism Algebra.TensorProduct.algEquivIncludeRange.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraSemiringAlgebra