Theorems · Theorem · category theory

MonoidHom.injective_of_surjective_of_injective_of_right_exact

∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : Group M₁]
  [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group N₁] [inst_4 : Group N₂] [inst_5 : Group N₃] (f₁ : M₁ →* M₂)
  (f₂ : M₂ →* M₃) (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.MulExact ⇑f₁ ⇑f₂ →
        Function.MulExact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₁ → Function.Injective ⇑i₂ → Function.Surjective ⇑f₂ → Function.Injective ⇑i₃

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

Defined in

Mathlib.Algebra.FiveLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupGroupGroupGroupGroup