Theorems · Theorem · linear algebra

TensorProduct.map_ker

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Surjective ⇑g →
      ∀ {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [inst_7 : AddCommGroup M'] [inst_8 : AddCommGroup N']
        [inst_9 : AddCommGroup P'] [inst_10 : Module R M'] [inst_11 : Module R N'] [inst_12 : Module R P']
        {f' : M' →ₗ[R] N'} {g' : N' →ₗ[R] P'},
        Function.Exact ⇑f' ⇑g' →
          Function.Surjective ⇑g' →
            (TensorProduct.map g g').ker = (LinearMap.lTensor N f').range ⊔ (LinearMap.rTensor N' f).range

Kernel of a product map (right-exactness of tensor product)

Defined in

Mathlib.LinearAlgebra.TensorProduct.RightExactness

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleAddCommGroupAddCommGroupAddCommGroupModuleModuleModule