Theorems · Definition · linear algebra

Submodule.lTensorOne

{R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (N : Submodule R S) → TensorProduct R ↥⊥ ↥N ≃ₗ[R] ↥N

If N is a submodule in an algebra S over R, there is the natural isomorphism of R-modules between i(R) ⊗[R] N and N induced by multiplication in S, here i : R → S is the structure map. This generalizes TensorProduct.lid as i(R) is not necessarily isomorphic to R.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Submodule

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra