mathlib documentation

category_theory.category.default

Categories

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
@[class]
structure category_theory.has_hom  :
Type uType (max u (v+1))
  • hom : obj → obj → Type ?

A 'notation typeclass' on the way to defining a category.

Instances
@[class]
structure category_theory.category_struct  :
Type uType (max u (v+1))

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

Instances
@[class]
structure category_theory.category  :
Type uType (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
def category_theory.large_category  :
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.

Instances
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} :
g = hf 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} :
(∀ {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} :
(∀ {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) :
((λ {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) :
((λ {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) :
(∀ {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) :
(∀ {Y : C} (g : Y X), g f = g)f = 𝟙 X

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} :
(X Y) → Prop
  • left_cancellation : ∀ {Z : C} (g h : Y Z), f g = f hg = h

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
@[class]
structure category_theory.mono {C : Type u} [category_theory.category C] {X Y : C} :
(X Y) → Prop
  • right_cancellation : ∀ {Z : C} (g h : Z X), g f = h fg = h

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

theorem category_theory.epi_comp {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) [category_theory.epi f] (g : Y Z) [category_theory.epi g] :

theorem category_theory.mono_comp {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) [category_theory.mono f] (g : Y Z) [category_theory.mono g] :

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] :

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] :

@[instance]

Equations

We now put a category instance on any preorder.

Because we do not allow the morphisms of a category to live in Prop, unfortunately we need to use plift and ulift when defining the morphisms.

As convenience functions, we provide hom_of_le and le_of_hom to wrap and unwrap inequalities.

@[instance]

The category structure coming from a preorder. There is a morphism X ⟶ Y if and only if X ≤ Y.

Because we don't allow morphisms to live in Prop, we have to define X ⟶ Y as ulift (plift (X ≤ Y)). See category_theory.hom_of_le and category_theory.le_of_hom.

See https://stacks.math.columbia.edu/tag/00D3.

Equations
def category_theory.hom_of_le {α : Type u} [preorder α] {U V : α} :
U V(U V)

Express an inequality as a morphism in the corresponding preorder category.

Equations
theorem category_theory.le_of_hom {α : Type u} [preorder α] {U V : α} :
(U V)U V

Extract the underlying inequality from a morphism in a preorder category.