Theorems · Theorem · category theory

MonoidHom.bijective_of_surjective_of_bijective_of_bijective_of_injective

∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {M₅ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7}
  {N₃ : Type u_8} {N₄ : Type u_9} {N₅ : Type u_10} [inst : Group M₁] [inst_1 : Group M₂] [inst_2 : Group M₃]
  [inst_3 : Group M₄] [inst_4 : Group M₅] [inst_5 : Group N₁] [inst_6 : Group N₂] [inst_7 : Group N₃]
  [inst_8 : Group N₄] [inst_9 : Group N₅] (f₁ : M₁ →* M₂) (f₂ : M₂ →* M₃) (f₃ : M₃ →* M₄) (f₄ : M₄ →* M₅)
  (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (g₃ : N₃ →* N₄) (g₄ : N₄ →* N₅) (i₁ : M₁ →* 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₃ →
        g₄.comp i₄ = i₅.comp f₄ →
          Function.MulExact ⇑f₁ ⇑f₂ →
            Function.MulExact ⇑f₂ ⇑f₃ →
              Function.MulExact ⇑f₃ ⇑f₄ →
                Function.MulExact ⇑g₁ ⇑g₂ →
                  Function.MulExact ⇑g₂ ⇑g₃ →
                    Function.MulExact ⇑g₃ ⇑g₄ →
                      Function.Surjective ⇑i₁ →
                        Function.Bijective ⇑i₂ →
                          Function.Bijective ⇑i₄ → Function.Injective ⇑i₅ → Function.Bijective ⇑i₃

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

Defined in

Mathlib.Algebra.FiveLemma

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupGroupGroupGroupGroupGroupGroupGroupGroupGroup