hasZeroObject — Mathlib

English

The category of differential objects has a zero object; it is the differential object with underlying zero object and zero differential.

Русский

Категория дифференциальных объектов имеет нулевой объект; это дифференциальный объект с нуловым базовым объектом и нулевым дифференциалом.

LaTeX

$$$\exists Z:\; \text{DifferentialObject}(S,C)\text{ such that } Z\text{ is zero object}$$$

Lean4

instance hasZeroObject : HasZeroObject (DifferentialObject S C) where
  zero :=
    ⟨{ obj := 0, d := 0 },
      { unique_to := fun X => ⟨⟨⟨{ f := 0 }⟩, fun f => by ext⟩⟩,
        unique_from := fun X => ⟨⟨⟨{ f := 0 }⟩, fun f => by ext⟩⟩ }⟩

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