Theorems · Definition · category theory

CategoryTheory.Limits.HasZeroObject.zeroIsInitial

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.Limits.IsInitial 0

A zero object is in particular initial.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Cited by: 5 results in Mathlib
Foundations: Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasZeroObject

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Limits.HasZeroObjectstatement and proof · cited by 1,298
CategoryTheory.Limits.IsInitialstatement · cited by 158
CategoryTheory.Limits.HasZeroObject.zero'statement · cited by 115
CategoryTheory.Limits.isZero_zeroproof · cited by 34
CategoryTheory.Limits.IsZero.isInitialproof · cited by 1

Cited by10

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.pushoutZeroZeroIsoproof · cited by 5
CategoryTheory.IsPushout.of_isBilimitproof · cited by 4
CategoryTheory.Limits.HasZeroObject.zeroIsoInitialproof · cited by 4
CategoryTheory.Subobject.botCoeIsoZeroproof · cited by 2
CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitialproof · cited by 2
CategoryTheory.MonoOver.botCoeIsoZeroproof · cited by 1
CategoryTheory.Limits.inl_pushoutZeroZeroIso_homproof · cited by 1
CategoryTheory.Limits.inr_pushoutZeroZeroIso_homproof · cited by 1
CategoryTheory.IsPushout.of_hasBinaryCoproductproof · cited by 0
CategoryTheory.Subobject.bot_eq_zeroproof · cited by 0