Theorems · Theorem · category theory

CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C],
  (∀ (A : C) (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f) → CategoryTheory.Limits.HasStrictInitialObjects C

If C has an initial object such that every morphism to it is an isomorphism, then C has strict initial objects.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Cited by

1 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasInitial