Theorems · Theorem · category theory

LinearMap.surjective_of_surjective_of_injective_of_left_exact

∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_7} {N₂ : Type u_8}
  {N₃ : Type u_9} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃]
  [inst_4 : Module R M₁] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁]
  [inst_8 : AddCommGroup N₂] [inst_9 : AddCommGroup N₃] [inst_10 : Module R N₁] [inst_11 : Module R N₂]
  [inst_12 : Module R N₃] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (i₁ : M₁ →ₗ[R] N₁)
  (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₂ → Function.Injective ⇑i₃ → Function.Injective ⇑g₁ → Function.Surjective ⇑i₁

A special case of one four lemma such that the left-most term is zero in terms of modules. For a diagram explaining the variables, see the module docstring.

Defined in

Mathlib.Algebra.FiveLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleAddCommGroupAddCommGroupAddCommGroupModuleModuleModule