mathlib documentation

category_theory.category.basic

Categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Notations #

Introduces notations

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

local notation f `  `:80 g:80 := category.comp g f    -- type as \oo

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 small_category, where v = u, which can be introduced as

universes u
variables {C : Type u} [small_category C]

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

universes u
variables {C : Type (u+1)} [large_category 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 can not be automatically inferred, through the category theory library we introduce universe parameters with morphism levels listed first, as in

universes v u

or

universes 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.

@[class]
structure category_theory.category (obj : Type u) :
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 large_category and small_category.)

See https://stacks.math.columbia.edu/tag/0014.

Instances of this typeclass
Instances of other typeclasses for category_theory.category
  • category_theory.category.has_sizeof_inst
@[simp]
theorem category_theory.category.id_comp {obj : Type u} [self : category_theory.category obj] {X Y : obj} (f : X Y) :
𝟙 X f = f
@[simp]
theorem category_theory.category.comp_id {obj : Type u} [self : category_theory.category obj] {X Y : obj} (f : X Y) :
f 𝟙 Y = f
@[simp]
theorem category_theory.category.assoc {obj : Type u} [self : category_theory.category obj] {W X Y Z : obj} (f : W X) (g : X Y) (h : Y Z) :
(f g) h = f g h
@[reducible]
def category_theory.large_category (C : Type (u+1)) :
Type (u+1)

A large_category 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.

@[reducible]

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

theorem category_theory.eq_whisker {C : Type u} [category_theory.category C] {X Y Z : C} {f g : X Y} (w : f = g) (h : Y Z) :
f h = g h

postcompose an equation between morphisms by another morphism

theorem category_theory.whisker_eq {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) {g h : Y Z} (w : g = h) :
f g = f h

precompose an equation between morphisms by another morphism

theorem category_theory.eq_of_comp_left_eq {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (w : {Z : C} (h : Y Z), f h = g h) :
f = g
theorem category_theory.eq_of_comp_right_eq {C : Type u} [category_theory.category C] {Y Z : C} {f g : Y Z} (w : {X : C} (h : X Y), h f = h g) :
f = g
theorem category_theory.eq_of_comp_left_eq' {C : Type u} [category_theory.category C] {X Y : C} (f g : X Y) (w : (λ {Z : C} (h : Y Z), f h) = λ {Z : C} (h : Y Z), g h) :
f = g
theorem category_theory.eq_of_comp_right_eq' {C : Type u} [category_theory.category C] {Y Z : C} (f g : Y Z) (w : (λ {X : C} (h : X Y), h f) = λ {X : C} (h : X Y), h g) :
f = g
theorem category_theory.id_of_comp_left_id {C : Type u} [category_theory.category C] {X : C} (f : X X) (w : {Y : C} (g : X Y), f g = g) :
f = 𝟙 X
theorem category_theory.id_of_comp_right_id {C : Type u} [category_theory.category C] {X : C} (f : X X) (w : {Y : C} (g : Y X), g f = g) :
f = 𝟙 X
theorem category_theory.comp_ite {C : Type u} [category_theory.category C] {P : Prop} [decidable P] {X Y Z : C} (f : X Y) (g g' : Y Z) :
f ite P g g' = ite P (f g) (f g')
theorem category_theory.ite_comp {C : Type u} [category_theory.category C] {P : Prop} [decidable P] {X Y Z : C} (f f' : X Y) (g : Y Z) :
ite P f f' g = ite P (f g) (f' g)
theorem category_theory.comp_dite {C : Type u} [category_theory.category C] {P : Prop} [decidable P] {X Y Z : C} (f : X Y) (g : P (Y Z)) (g' : ¬P (Y Z)) :
f dite P (λ (h : P), g h) (λ (h : ¬P), g' h) = dite P (λ (h : P), f g h) (λ (h : ¬P), f g' h)
theorem category_theory.dite_comp {C : Type u} [category_theory.category C] {P : Prop} [decidable P] {X Y Z : C} (f : P (X Y)) (f' : ¬P (X Y)) (g : Y Z) :
dite P (λ (h : P), f h) (λ (h : ¬P), f' h) g = dite P (λ (h : P), f h g) (λ (h : ¬P), f' h g)
@[class]
structure category_theory.epi {C : Type u} [category_theory.category 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.

See https://stacks.math.columbia.edu/tag/003B.

Instances of this typeclass
@[class]
structure category_theory.mono {C : Type u} [category_theory.category 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.

See https://stacks.math.columbia.edu/tag/003B.

Instances of this typeclass
theorem category_theory.cancel_epi {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) [category_theory.epi f] {g h : Y Z} :
f g = f h g = h
theorem category_theory.cancel_mono {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) [category_theory.mono f] {g h : Z X} :
g f = h f g = h
theorem category_theory.cancel_epi_id {C : Type u} [category_theory.category C] {X Y : C} (f : X Y) [category_theory.epi f] {h : Y Y} :
f h = f h = 𝟙 Y
theorem category_theory.cancel_mono_id {C : Type u} [category_theory.category C] {X Y : C} (f : X Y) [category_theory.mono f] {g : X X} :
g f = f g = 𝟙 X
@[instance]
theorem category_theory.mono_of_mono {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) (g : Y Z) [category_theory.mono (f g)] :
theorem category_theory.mono_of_mono_fac {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : Y Z} {h : X Z} [category_theory.mono h] (w : f g = h) :
theorem category_theory.epi_of_epi {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) (g : Y Z) [category_theory.epi (f g)] :
theorem category_theory.epi_of_epi_fac {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : Y Z} {h : X Z} [category_theory.epi h] (w : f g = h) :
@[protected, instance]
Equations

Many proofs in the category theory library use the dsimp, simp pattern, which typically isn't necessary elsewhere.

One would usually hope that the same effect could be achieved simply with simp.

The essential issue is that composition of morphisms involves dependent types. When you have a chain of morphisms being composed, say f : X ⟶ Y and g : Y ⟶ Z, then simp can operate succesfully on the morphisms (e.g. if f is the identity it can strip that off).

However if we have an equality of objects, say Y = Y', then simp can't operate because it would break the typing of the composition operations. We rarely have interesting equalities of objects (because that would be "evil" --- anything interesting should be expressed as an isomorphism and tracked explicitly), except of course that we have plenty of definitional equalities of objects.

dsimp can apply these safely, even inside a composition.

After dsimp has cleared up the object level, simp can resume work on the morphism level --- but without the dsimp step, because simp looks at expressions syntactically, the relevant lemmas might not fire.

There's no bound on how many times you potentially could have to switch back and forth, if the simp introduced new objects we again need to dsimp. In practice this does occur, but only rarely, because simp tends to shorten chains of compositions (i.e. not introduce new objects at all).