Theorems · Definition · commutative algebra

TensorProduct.mapIncl

{R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_9} →
      {Q : Type u_10} →
        [inst_1 : AddCommMonoid P] →
          [inst_2 : AddCommMonoid Q] →
            [inst_3 : Module R P] →
              [inst_4 : Module R Q] →
                (p : Submodule R P) → (q : Submodule R Q) → TensorProduct R ↥p ↥q →ₗ[R] TensorProduct R P Q

Given submodules p ⊆ P and q ⊆ Q, this is the natural map: p ⊗ q → P ⊗ Q.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Map

Cited by

14 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule