Theorems · Definition · commutative algebra

Subalgebra.rTensorBot

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (A : Subalgebra R S) → TensorProduct R ↥A ↥⊥ ≃ₐ[R] ↥A

If A is a subalgebra of S/R, there is the natural R-algebra isomorphism between A ⊗[R] i(R) and A induced by multiplication in S, here i : R → S is the structure map. This generalizes Algebra.TensorProduct.rid as i(R) is not necessarily isomorphic to R. This is the Subalgebra version of Submodule.rTensorOne

Defined in

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra