Theorems · Theorem · category theory

MonoidHom.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 : Group M₁] [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group M₄] [inst_4 : Group N₁]
  [inst_5 : Group N₂] [inst_6 : Group N₃] [inst_7 : Group 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.MulExact ⇑f₂ ⇑f₃ →
          Function.MulExact ⇑g₁ ⇑g₂ →
            Function.MulExact ⇑g₂ ⇑g₃ →
              Function.Surjective ⇑i₁ → Function.Surjective ⇑i₃ → Function.Injective ⇑i₄ → Function.Surjective ⇑i₂

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

Defined in

Mathlib.Algebra.FiveLemma

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupGroupGroupGroupGroupGroupGroupGroup