hasZeroObject — Mathlib

English

If C has a zero object and zero morphisms, then the graded object category GradedObject β C also has a zero object for any index β; i.e., there is a zero object in GradedObject β C built componentwise from the zero objects of C.

Русский

Если в C имеется нулевой объект и нулевые морфизмы, то и в GradedObject β C существует нулевой объект, компонентно задаваемый нулевыми объектами C.

LaTeX

$$$\text{HasZeroObject (GradedObject β C)}$$$

Lean4

instance hasZeroObject [HasZeroObject C] [HasZeroMorphisms C] (β : Type w) :
    HasZeroObject.{max w v} (GradedObject β C) := by
  refine ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩⟩⟩ <;> cat_disch

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