Categories

Defines a category, as a type class parametrised by the type of objects.

Notation

Introduces notations in the CategoryTheory scope

• X ⟶ Y for the morphism spaces (type as \hom),
• 𝟙 X for the identity morphism on X (type as \b1),
• f ≫ g for composition in the 'arrows' convention (type as \gg).

Users may like to add g ⊚ f for composition in the standard convention, using

local notation:80 g " ⊚ " f:80 => CategoryTheory.CategoryStruct.comp f g    -- type as \oo

def LibraryNote.category_theory_universes : Batteries.Util.LibraryNote

The typeclass Category C describes morphisms associated to objects of type C : Type u.

The universe levels of the objects and morphisms are independent, and will often need to be specified explicitly, as Category.{v} C.

Typically any concrete example will either be a SmallCategory, where v = u, which can be introduced as

universe u
variable {C : Type u} [SmallCategory C]

or a LargeCategory, where u = v+1, which can be introduced as

universe u
variable {C : Type (u+1)} [LargeCategory C]

In order for the library to handle these cases uniformly, we generally work with the unconstrained Category.{v u}, for which objects live in Type u and morphisms live in Type v.

Because the universe parameter u for the objects can be inferred from C when we write Category C, while the universe parameter v for the morphisms cannot be automatically inferred, through the category theory library we introduce universe parameters with morphism levels listed first, as in

universe v u

or

universe v₁ v₂ u₁ u₂

when multiple independent universes are needed.

This has the effect that we can simply write Category.{v} C (that is, only specifying a single parameter) while u will be inferred.

Often, however, it's not even necessary to include the .{v}. (Although it was in earlier versions of Lean.) If it is omitted a "free" universe will be used.

Equations

• LibraryNote.category_theory_universes = default

def LibraryNote.universe_output_parameters_and_typeclass_caching : Batteries.Util.LibraryNote

Many classes in Mathlib have universe parameters that do not appear in their input parameter types. For example:

• Category.{v} (C : Type u) — the morphism universe v is not determined by C
• HasLimitsOfSize.{v₁, u₁} (C : Type u) [Category.{v} C] — the shape universes v₁, u₁ are not determined by C
• Small.{w} (α : Type v) — the target universe w is not determined by α (but v is determined by α, so v is an output)
• Functor.IsContinuous.{t} (F) (J) (K) — the sheaf type universe t is not determined by F, J, K
• UnivLE.{u, v} — has no input parameters at all

By default (since https://github.com/leanprover/lean4/pull/12286), Lean treats any universe parameter not occurring in input types as an output parameter, and erases it from typeclass resolution cache keys. This means that queries differing only in such a universe share a cache entry — the first result found is reused.

This is correct when the universe truly is determined by the inputs (e.g., v in Small.{w} (α : Type v)), but incorrect when the universe is part of the question (e.g., v in Category.{v} C). Cache collisions cause "stuck at solving universe constraint" errors or silent misresolution.

The @[univ_out_params] attribute (from https://github.com/leanprover/lean4/pull/12423) overrides the default:

• @[univ_out_params] — no universe parameters are output (all kept in cache key)
• @[univ_out_params v] — only v is output

Rule of thumb: if the class is typically used with explicit universe annotations (e.g., HasLimitsOfSize.{v₁, u₁} C) or is marked @[pp_with_univ], its "extra" universe parameters are likely inputs, not outputs, and the class should be annotated with @[univ_out_params].

Equations

• LibraryNote.universe_output_parameters_and_typeclass_caching = default

class CategoryTheory.CategoryStruct (obj : Type u) extends Quiver obj : Type (max u (v + 1))

A preliminary structure on the way to defining a category, containing the data, but none of the axioms.

• Hom : obj → obj → Type v
• id (X : obj) : X ⟶ X

  The identity morphism on an object.

• comp {X Y Z : obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)

  Composition of morphisms in a category, written f ≫ g.

def CategoryTheory.«term𝟙» : Lean.ParserDescr

Notation for the identity morphism in a category.

Equations

• CategoryTheory.«term𝟙» = Lean.ParserDescr.node `CategoryTheory.«term𝟙» 1024 (Lean.ParserDescr.symbol "𝟙")

def CategoryTheory.«term_≫_» : Lean.TrailingParserDescr

Notation for composition of morphisms in a category.

Equations

• CategoryTheory.«term_≫_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_≫_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ ") (Lean.ParserDescr.cat `term 80))

def CategoryTheory.sorryIfSorry : Lean.ParserDescr

Close the main goal with sorry if its type contains sorry, and fail otherwise.

Equations

• CategoryTheory.sorryIfSorry = Lean.ParserDescr.node `CategoryTheory.sorryIfSorry 1024 (Lean.ParserDescr.nonReservedSymbol "sorry_if_sorry" false)

def CategoryTheory.evalSorryIfSorry : Lean.Elab.Tactic.Tactic

Close the main goal with sorry if its type contains sorry, and fail otherwise.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.rfl_cat : Lean.ParserDescr

rfl_cat is a macro for intros; rfl which is attempted in aesop_cat before doing the more expensive aesop tactic.

This gives a speedup because simp (called by aesop) can be very slow. https://github.com/leanprover-community/mathlib4/pull/25475 contains measurements from June 2025.

Implementation notes:

• refine id ?_: In some cases it is important that the type of the proof matches the expected type exactly. e.g. if the goal is 2 = 1 + 1, the rfl tactic will give a proof of type 2 = 2. Starting a proof with refine id ?_ is a trick to make sure that the proof has exactly the expected type, in this case 2 = 1 + 1. See also https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/changing.20a.20proof.20can.20break.20a.20later.20proof
• apply_rfl: rfl is a macro that attempts both eq_refl and apply_rfl. Since apply_rfl subsumes eq_refl, we can use apply_rfl instead. This fails twice as fast as rfl.

Equations

• CategoryTheory.rfl_cat = Lean.ParserDescr.node `CategoryTheory.rfl_cat 1024 (Lean.ParserDescr.nonReservedSymbol "rfl_cat" false)

def CategoryTheory.aesop_cat : Lean.ParserDescr

A thin wrapper for aesop which adds the CategoryTheory rule set and allows aesop to look through semireducible definitions when calling intros. This tactic fails when it is unable to solve the goal, making it suitable for use in auto-params.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.aesop_cat? : Lean.ParserDescr

We also use aesop_cat? to pass along a Try this suggestion when using aesop_cat

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.aesop_cat_nonterminal : Lean.ParserDescr

A variant of aesop_cat which does not fail when it is unable to solve the goal. Use this only for exploration! Nonterminal aesop is even worse than nonterminal simp.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.categoryTheoryDischarger : Lean.Elab.Tactic.TacticM Unit

A tactic for discharging easy category theory goals, widely used as an autoparameter. Currently this defaults to the aesop_cat wrapper around aesop, but by setting the option mathlib.tactic.category.grind to true, it will use the grind tactic instead.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.cat_disch : Lean.ParserDescr

A tactic for discharging easy category theory goals, widely used as an autoparameter. Currently this defaults to the aesop_cat wrapper around aesop, but by setting the option mathlib.tactic.category.grind to true, it will use the grind tactic instead.

Equations

• CategoryTheory.cat_disch = Lean.ParserDescr.node `CategoryTheory.cat_disch 1024 (Lean.ParserDescr.nonReservedSymbol "cat_disch" false)

class CategoryTheory.Category (obj : Type u) extends CategoryTheory.CategoryStruct.{v, u} obj : Type (max u (v + 1))

The typeclass Category C describes morphisms associated to objects of type C. The universe levels of the objects and morphisms are unconstrained, and will often need to be specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.)

• Hom : obj → obj → Type v
• id (X : obj) : X ⟶ X
• comp {X Y Z : obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
• id_comp {X Y : obj} (f : X ⟶ Y) : CategoryStruct.comp (CategoryStruct.id X) f = f

  Identity morphisms are left identities for composition.

• comp_id {X Y : obj} (f : X ⟶ Y) : CategoryStruct.comp f (CategoryStruct.id Y) = f

  Identity morphisms are right identities for composition.

• assoc {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g) h = CategoryStruct.comp f (CategoryStruct.comp g h)

  Composition in a category is associative.

@[reducible, inline]

abbrev CategoryTheory.LargeCategory (C : Type (u + 1)) : Type (u + 1)

A LargeCategory has objects in one universe level higher than the universe level of the morphisms. It is useful for examples such as the category of types, or the category of groups, etc.

Equations

• CategoryTheory.LargeCategory C = CategoryTheory.Category.{?u.7, ?u.7 + 1} C

@[reducible, inline]

abbrev CategoryTheory.SmallCategory (C : Type u) : Type (u + 1)

A SmallCategory has objects and morphisms in the same universe level.

Equations

• CategoryTheory.SmallCategory C = CategoryTheory.Category.{?u.7, ?u.7} C

theorem CategoryTheory.Category.assoc' {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ X) (h : Z ⟶ Y) : CategoryStruct.comp h (CategoryStruct.comp g f) = CategoryStruct.comp (CategoryStruct.comp h g) f

theorem CategoryTheory.eq_whisker {C : Type u} [Category.{v, u} C] {X Y Z : C} {f g : X ⟶ Y} (w : f = g) (h : Y ⟶ Z) : CategoryStruct.comp f h = CategoryStruct.comp g h

Postcompose an equation between morphisms by another morphism

theorem CategoryTheory.whisker_eq {C : Type u} [Category.{v, u} C] {X Y Z : C} {f g : Y ⟶ X} (h : Z ⟶ Y) (w : f = g) : CategoryStruct.comp h f = CategoryStruct.comp h g

Precompose an equation between morphisms by another morphism

def CategoryTheory.«term_=≫_» : Lean.TrailingParserDescr

Notation for whiskering an equation by a morphism (on the right). If f g : X ⟶ Y and w : f = g and h : Y ⟶ Z, then w =≫ h : f ≫ h = g ≫ h.

Equations

• CategoryTheory.«term_=≫_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_=≫_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =≫ ") (Lean.ParserDescr.cat `term 80))

def CategoryTheory.«term_≫=_» : Lean.TrailingParserDescr

Notation for whiskering an equation by a morphism (on the left). If g h : Y ⟶ Z and w : g = h and f : X ⟶ Y, then f ≫= w : f ≫ g = f ≫ h.

Equations

• CategoryTheory.«term_≫=_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_≫=_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫= ") (Lean.ParserDescr.cat `term 80))

theorem CategoryTheory.eq_of_comp_left_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), CategoryStruct.comp f h = CategoryStruct.comp g h) : f = g

theorem CategoryTheory.eq_of_comp_right_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f g : Y ⟶ X} (w : ∀ {Z : C} (h : Z ⟶ Y), CategoryStruct.comp h f = CategoryStruct.comp h g) : f = g

theorem CategoryTheory.eq_of_comp_left_eq' {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) (w : (fun {Z : C} (h : Y ⟶ Z) => CategoryStruct.comp f h) = fun {Z : C} (h : Y ⟶ Z) => CategoryStruct.comp g h) : f = g

theorem CategoryTheory.eq_of_comp_right_eq' {C : Type u} [Category.{v, u} C] {X Y : C} (f g : Y ⟶ X) (w : (fun {Z : C} (h : Z ⟶ Y) => CategoryStruct.comp h f) = fun {Z : C} (h : Z ⟶ Y) => CategoryStruct.comp h g) : f = g

theorem CategoryTheory.id_of_comp_left_id {C : Type u} [Category.{v, u} C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), CategoryStruct.comp f g = g) : f = CategoryStruct.id X

theorem CategoryTheory.id_of_comp_right_id {C : Type u} [Category.{v, u} C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), CategoryStruct.comp g f = g) : f = CategoryStruct.id X

theorem CategoryTheory.comp_ite {C : Type u} [Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z) : CategoryStruct.comp f (if P then g else g') = if P then CategoryStruct.comp f g else CategoryStruct.comp f g'

theorem CategoryTheory.ite_comp {C : Type u} [Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (g g' : Z ⟶ Y) (f : Y ⟶ X) : CategoryStruct.comp (if P then g else g') f = if P then CategoryStruct.comp g f else CategoryStruct.comp g' f

theorem CategoryTheory.comp_dite {C : Type u} [Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) : CategoryStruct.comp f (if h : P then g h else g' h) = if h : P then CategoryStruct.comp f (g h) else CategoryStruct.comp f (g' h)

theorem CategoryTheory.dite_comp {C : Type u} [Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (g : P → (Z ⟶ Y)) (g' : ¬P → (Z ⟶ Y)) (f : Y ⟶ X) : CategoryStruct.comp (if h : P then g h else g' h) f = if h : P then CategoryStruct.comp (g h) f else CategoryStruct.comp (g' h) f

class CategoryTheory.Epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop

A morphism f is an epimorphism if it can be cancelled when precomposed: f ≫ g = f ≫ h implies g = h.

Stacks Tag 003B

• left_cancellation {Z : C} (g h : Y ⟶ Z) : CategoryStruct.comp f g = CategoryStruct.comp f h → g = h

  A morphism f is an epimorphism if it can be cancelled when precomposed.

class CategoryTheory.Mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop

A morphism f is a monomorphism if it can be cancelled when postcomposed: g ≫ f = h ≫ f implies g = h.

Stacks Tag 003B

• right_cancellation {Z : C} (g h : Z ⟶ X) : CategoryStruct.comp g f = CategoryStruct.comp h f → g = h

  A morphism f is a monomorphism if it can be cancelled when postcomposed.

instance CategoryTheory.instEpiId {C : Type u} [Category.{v, u} C] (X : C) : Epi (CategoryStruct.id X)

instance CategoryTheory.instMonoId {C : Type u} [Category.{v, u} C] (X : C) : Mono (CategoryStruct.id X)

theorem CategoryTheory.cancel_epi {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [Epi f] {g h : Y ⟶ Z} : CategoryStruct.comp f g = CategoryStruct.comp f h ↔ g = h

theorem CategoryTheory.cancel_mono {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : Y ⟶ X) [Mono f] {g h : Z ⟶ Y} : CategoryStruct.comp g f = CategoryStruct.comp h f ↔ g = h

theorem CategoryTheory.cancel_epi_assoc_iff {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [Epi f] {g h : Y ⟶ Z} {W : C} {k l : Z ⟶ W} : CategoryStruct.comp (CategoryStruct.comp f g) k = CategoryStruct.comp (CategoryStruct.comp f h) l ↔ CategoryStruct.comp g k = CategoryStruct.comp h l

theorem CategoryTheory.cancel_mono_assoc_iff {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : Y ⟶ X) [Mono f] {g h : Z ⟶ Y} {W : C} {k u : W ⟶ Z} : CategoryStruct.comp k (CategoryStruct.comp g f) = CategoryStruct.comp u (CategoryStruct.comp h f) ↔ CategoryStruct.comp k g = CategoryStruct.comp u h

theorem CategoryTheory.cancel_epi_id {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Epi f] {h : Y ⟶ Y} : CategoryStruct.comp f h = f ↔ h = CategoryStruct.id Y

theorem CategoryTheory.cancel_mono_id {C : Type u} [Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [Mono f] {h : Y ⟶ Y} : CategoryStruct.comp h f = f ↔ h = CategoryStruct.id Y

instance CategoryTheory.epi_comp {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [Epi f] (g : Y ⟶ Z) [Epi g] : Epi (CategoryStruct.comp f g)

The composition of epimorphisms is again an epimorphism. This version takes Epi f and Epi g as typeclass arguments. For a version taking them as explicit arguments, see epi_comp'.

instance CategoryTheory.mono_comp {C : Type u} [Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) [Mono g] (f : Y ⟶ X) [Mono f] : Mono (CategoryStruct.comp g f)

The composition of monomorphisms is again a monomorphism. This version takes Mono f and Mono g as typeclass arguments. For a version taking them as explicit arguments, see mono_comp'.

theorem CategoryTheory.epi_comp' {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) : Epi (CategoryStruct.comp f g)

The composition of epimorphisms is again an epimorphism. This version takes Epi f and Epi g as explicit arguments. For a version taking them as typeclass arguments, see epi_comp.

theorem CategoryTheory.mono_comp' {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (hg : Mono g) (hf : Mono f) : Mono (CategoryStruct.comp g f)

The composition of monomorphisms is again a monomorphism. This version takes Mono f and Mono g as explicit arguments. For a version taking them as typeclass arguments, see mono_comp.

theorem CategoryTheory.epi_of_epi {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi (CategoryStruct.comp f g)] : Epi g

theorem CategoryTheory.mono_of_mono {C : Type u} [Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X) [Mono (CategoryStruct.comp g f)] : Mono g

theorem CategoryTheory.epi_of_epi_fac {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Epi h] (w : CategoryStruct.comp f g = h) : Epi g

theorem CategoryTheory.mono_of_mono_fac {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} {h : Z ⟶ X} [Mono h] (w : CategoryStruct.comp g f = h) : Mono g

theorem CategoryTheory.epi_iff_forall_injective {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Epi f ↔ ∀ (Z : C), Function.Injective fun (g : Y ⟶ Z) => CategoryStruct.comp f g

f : X ⟶ Y is an epimorphism iff for all Z, composition of morphisms Y ⟶ Z with f is injective.

theorem CategoryTheory.mono_iff_forall_injective {C : Type u} [Category.{v, u} C] {X Y : C} (f : Y ⟶ X) : Mono f ↔ ∀ (Z : C), Function.Injective fun (g : Z ⟶ Y) => CategoryStruct.comp g f

f : X ⟶ Y is a monomorphism iff for all Z, composition of morphisms Z ⟶ X with f is injective.

instance CategoryTheory.instEpiOfIsThin {C : Type u} [Category.{v, u} C] {X Y : C} [Quiver.IsThin C] (f : X ⟶ Y) : Epi f

instance CategoryTheory.instMonoOfIsThin {C : Type u} [Category.{v, u} C] {X Y : C} [Quiver.IsThin C] (f : Y ⟶ X) : Mono f

@[instance_reducible]

def CategoryTheory.uliftCategory (C : Type u) [Category.{v, u} C] : Category.{v, max u' u} (ULift.{u', u} C)

The category structure on ULift C that is induced from the category structure on C. This is not made a global instance because of a diamond when C is a preordered type.

Equations

• One or more equations did not get rendered due to their size.