Theorems · Inductive type · category theory

CategoryTheory.Limits.InitialMonoClass

(C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop

A category is an InitialMonoClass if the canonical morphism of an initial object is a monomorphism. In practice, this is most useful when given an arbitrary morphism out of the chosen initial object, see initial.mono_from. Given a terminal object, this is equivalent to the assumption that the unique morphism from initial to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category. TODO: This is a condition satisfied by categories with zero objects and morphisms.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Cited by

12 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.Category