Theorems · Theorem · category theory

AddMonoidHom.surjective_of_surjective_of_surjective_of_injective

∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8}
  {N₄ : Type u_9} [inst : AddGroup M₁] [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃] [inst_3 : AddGroup M₄]
  [inst_4 : AddGroup N₁] [inst_5 : AddGroup N₂] [inst_6 : AddGroup N₃] [inst_7 : AddGroup N₄] (f₁ : M₁ →+ M₂)
  (f₂ : M₂ →+ M₃) (f₃ : M₃ →+ M₄) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (g₃ : N₃ →+ N₄) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂)
  (i₃ : M₃ →+ N₃) (i₄ : M₄ →+ N₄),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      g₃.comp i₃ = i₄.comp f₃ →
        Function.Exact ⇑f₂ ⇑f₃ →
          Function.Exact ⇑g₁ ⇑g₂ →
            Function.Exact ⇑g₂ ⇑g₃ →
              Function.Surjective ⇑i₁ → Function.Surjective ⇑i₃ → Function.Injective ⇑i₄ → Function.Surjective ⇑i₂

One four lemma in terms of additive groups. For a diagram explaining the variables, see the module docstring.

Defined in

Mathlib.Algebra.FiveLemma

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddGroupAddGroupAddGroupAddGroupAddGroupAddGroup