isZero — Mathlib

English

For X ≅ Y, IsZero X ↔ IsZero Y.

Русский

Для X ≅ Y верно IsZero X ⇔ IsZero Y.

LaTeX

$$$\\\\text{IsZero}(X) \\\\iff \\\\text{IsZero}(Y) \text{ for } X \\cong Y$$$

Lean4

theorem isZero (F : C ⥤ D) (hF : ∀ X, IsZero (F.obj X)) : IsZero F :=
  by
  constructor <;> intro G <;> refine ⟨⟨⟨?_⟩, ?_⟩⟩
  · refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_src _ _
  · intro f
    ext
    apply (hF _).eq_of_src _ _
  · refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_tgt _ _
  · intro f
    ext
    apply (hF _).eq_of_tgt _ _

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