Theorems · Theorem · category theory

MonoidHom.mulExact_iff_of_surjective_of_bijective_of_injective

∀ {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} {N₃ : Type u_13}
  [inst : CommMonoid M₁] [inst_1 : CommMonoid M₂] [inst_2 : CommMonoid M₃] [inst_3 : CommMonoid N₁]
  [inst_4 : CommMonoid N₂] [inst_5 : CommMonoid N₃] (f : M₁ →* M₂) (g : M₂ →* M₃) (f' : N₁ →* N₂) (g' : N₂ →* N₃)
  (τ₁ : M₁ →* N₁) (τ₂ : M₂ →* N₂) (τ₃ : M₃ →* N₃),
  f'.comp τ₁ = τ₂.comp f →
    g'.comp τ₂ = τ₃.comp g →
      Function.Surjective ⇑τ₁ →
        Function.Bijective ⇑τ₂ → Function.Injective ⇑τ₃ → (Function.MulExact ⇑f ⇑g ↔ Function.MulExact ⇑f' ⇑g')

When we have a commutative diagram from a sequence of two maps to another, such that the left vertical map is surjective, the middle vertical map is bijective and the right vertical map is injective, then the upper row is exact iff the lower row is. See ShortComplex.exact_iff_of_epi_of_isIso_of_mono in the file Mathlib/Algebra/Homology/ShortComplex/Exact.lean for the categorical version of this result.

Defined in

Mathlib.Algebra.Exact.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoidCommMonoidCommMonoidCommMonoidCommMonoid