Categories

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

Notations

Introduces notations

X ⟶ Y for the morphism spaces,
f ≫ g for composition in the 'arrows' convention.

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

source

@[class]

structure category_theory.has_hom :

Type u → Type (max u (v+1))

hom : obj → obj → Type ?

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

Instances

source

@[class]

structure category_theory.category_struct :

Type u → Type (max u (v+1))

to_has_hom : category_theory.has_hom obj
id : Π (X : obj), X ⟶ X
comp : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)

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

Instances

source

@[class]

structure category_theory.category :

Type u → Type (max u (v+1))

to_category_struct : category_theory.category_struct obj
id_comp' : (∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f) . "obviously"
comp_id' : (∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f) . "obviously"
assoc' : (∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h) . "obviously"

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

Instances

source

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

category_theory.types
Mon.large_category
AddMon.large_category
CommMon.large_category
AddCommMon.large_category
Group.large_category
AddGroup.large_category
CommGroup.large_category
AddCommGroup.large_category
SemiRing.large_category
Ring.large_category
CommSemiRing.large_category
CommRing.large_category
Top.large_category
category_theory.Cat.category
category_theory.Groupoid.category
category_theory.rel
Meas.large_category
Preorder.large_category
PartialOrder.large_category
LinearOrder.large_category
NonemptyFinLinOrd.large_category
UniformSpace.large_category
CpltSepUniformSpace.category

source

def category_theory.small_category :

Type u → Type (u+1)

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

Instances

source

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

source

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

g = h → f ≫ g = f ≫ h

precompose an equation between morphisms by another morphism

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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)

source

@[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 ≫ h → g = h

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

Instances

source

@[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 ≫ f → g = h

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

Instances

source

@[instance]

def category_theory.category_theory.epi {C : Type u} [category_theory.category C] (X : C) :

category_theory.epi (𝟙 X)

Equations

_ = _

source

@[instance]

def category_theory.category_theory.mono {C : Type u} [category_theory.category C] (X : C) :

category_theory.mono (𝟙 X)

Equations

_ = _

source

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

source

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

source

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

source

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

source

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

category_theory.epi (f ≫ g)

source

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

category_theory.mono (f ≫ g)

source

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

category_theory.mono f

source

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

f ≫ g = h → category_theory.mono f

source

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

category_theory.epi g

source

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

f ≫ g = h → category_theory.epi g

source

@[instance]

def category_theory.ulift_category (C : Type u) [category_theory.category C] :

category_theory.category (ulift C)

Equations

category_theory.ulift_category C = {to_category_struct := {to_has_hom := {hom := λ (X Y : ulift C), X.down ⟶ Y.down}, id := λ (X : ulift C), 𝟙 X.down, comp := λ (_x _x_1 _x_2 : ulift C) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), f ≫ g}, id_comp' := _, comp_id' := _, assoc' := _}

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.

source

@[instance]

def preorder.small_category (α : Type u) [preorder α] :

category_theory.small_category α

Equations

preorder.small_category α = {to_category_struct := {to_has_hom := {hom := λ (U V : α), ulift (plift (U ≤ V))}, id := λ (X : α), {down := {down := _}}, comp := λ (X Y Z : α) (f : X ⟶ Y) (g : Y ⟶ Z), {down := {down := _}}}, id_comp' := _, comp_id' := _, assoc' := _}

source

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

category_theory.hom_of_le h = {down := {down := h}}

source

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.

mathlib documentation

category_theory.category.default

Categories

Notations

General documentation

Additional documentation

Library

mathlib documentation

category_theory.​category.​default

Categories

Notations

General documentation

Additional documentation

Library

category_theory.category.default