hasZeroObject_of_additive — Mathlib

English

If C has a zero object and F: C → D is additive, then D has a zero object given by F(0_C).

Русский

Если в C есть нулевой объект и F: C → D аддитивен, то в D существует нулевой объект, равный F(0_C).

LaTeX

$$$\text{HasZeroObject}(C) \Rightarrow \text{HasZeroObject}(D) \text{ with } 0_D := F(0_C)$$$

Lean4

theorem hasZeroObject_of_additive [HasZeroObject C] : HasZeroObject D where
  zero := ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩

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