Theorems · Theorem · commutative algebra

IsTensorProduct.map_injective_of_flat_left_right

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₁ : Type u_7}
  {N₂ : Type u_8} [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₁] [inst_8 : Module R M₂]
  [inst_9 : AddCommMonoid N₁] [inst_10 : AddCommMonoid N₂] [inst_11 : Module R N₁] [inst_12 : Module R N₂]
  {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g)
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂),
  Function.Injective ⇑i₁ →
    Function.Injective ⇑i₂ → ∀ [Module.Flat R M₁] [Module.Flat R N₂], Function.Injective ⇑(hf.map hg i₁ i₂)

If M₁ and N₂ are flat R-modules, i₁ : M₁ →ₗ[R] N₁ and i₂ : M₂ →ₗ[R] N₂ are injective linear maps, then the linear map i : M ≅ M₁ ⊗[R] M₂ →ₗ[R] N₁ ⊗[R] N₂ ≅ N induced by i₁ and i₂ is injective. See IsTensorProduct.map_injective_of_flat for different flatness conditions.

Defined in

Mathlib.RingTheory.Flat.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModuleAddCommMonoidAddCommMonoidModuleModuleAddCommMonoidAddCommMonoidModuleModuleModule.FlatModule.Flat