Theorems · Theorem · commutative algebra

lTensor_injective_of_exact_of_exact_of_rTensor_injective

∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N₁ : Type u_8} {N₂ : Type u_9}
  {N₃ : Type u_10} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  {f₁ : M₁ →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {g₁ : N₁ →ₗ[R] N₂} {g₂ : N₂ →ₗ[R] N₃},
  Function.Exact ⇑f₁ ⇑f₂ →
    Function.Surjective ⇑f₂ →
      Function.Exact ⇑g₁ ⇑g₂ →
        Function.Surjective ⇑g₂ →
          Function.Injective ⇑(LinearMap.rTensor N₃ f₁) →
            Function.Injective ⇑(LinearMap.lTensor M₂ g₁) → Function.Injective ⇑(LinearMap.lTensor M₃ g₁)

Given M₁ → M₂ → M₃ → 0 and N₁ → N₂ → N₃ → 0, if M₁ ⊗ N₃ → M₂ ⊗ N₃ and M₂ ⊗ N₁ → M₂ ⊗ N₂ are both injective, then M₃ ⊗ N₁ → M₃ ⊗ N₂ is also injective.

Defined in

Mathlib.RingTheory.LocalRing.Module

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupModule