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 (obj : Type u) :
Type (max u (v+1))
  • hom : obj → obj → Type ?

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

Instances
@[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
@[simp]
theorem category_theory.category.id_comp {obj : Type u} [c : category_theory.category obj] {X Y : obj} (f : X Y) :
𝟙 X f = f

@[simp]
theorem category_theory.category.comp_id {obj : Type u} [c : category_theory.category obj] {X Y : obj} (f : X Y) :
f 𝟙 Y = f

@[simp]
theorem category_theory.category.assoc {obj : Type u} [c : category_theory.category obj] {W X Y Z : obj} (f : W X) (g : X Y) (h : Y Z) :
(f g) h = f g h

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_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
  • 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} (f : 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] (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) :

@[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 : α} (h : 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 : α} (h : U V) :
U V

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