tfae_mono — Mathlib

English

For any morphism f: X → Y and any Z, the three statements Mono(f), kernel.ι_f = 0, and the exactness of (0 → Z → X → Y) are equivalent.

Русский

Для любого морфизма f: X → Y и любого Z утверждения Mono(f), kernel.ι_f = 0 и точность (0 → X → Y) эквивалентны.

LaTeX

$$TFAE [Mono f, kernel.ι f = 0, (ShortComplex.mk (0 : Z ⟶ X) f zero_comp).Exact]$$

Lean4

theorem tfae_mono {X Y : C} (f : X ⟶ Y) (Z : C) :
    TFAE [Mono f, kernel.ι f = 0, (ShortComplex.mk (0 : Z ⟶ X) f zero_comp).Exact] :=
  by
  tfae_have 2 → 1 := mono_of_kernel_ι_eq_zero _
  tfae_have 1 → 2
    | _ => by rw [← cancel_mono f, kernel.condition, zero_comp]
  tfae_have 3 ↔ 1 := ShortComplex.exact_iff_mono _ (by simp)
  tfae_finish

Похожие утверждения