mathlib documentation

category_theory.category.basic

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
source
@[class]
structure category_theory.category_struct (obj : Type u) :
Type (max u (v+1))
  • to_quiver : quiver 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 of this typeclass
Instances of other typeclasses for category_theory.category_struct
  • category_theory.category_struct.has_sizeof_inst
source
@[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
source
@[simp]
theorem category_theory.category.id_comp {obj : Type u} [self : category_theory.category obj] {X Y : obj} (f : X ⟶ Y) :
𝟙 X ≫ f = f
source
@[simp]
theorem category_theory.category.comp_id {obj : Type u} [self : category_theory.category obj] {X Y : obj} (f : X ⟶ Y) :
f ≫ 𝟙 Y = f
source
@[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
source
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.

source
def category_theory.small_category (C : Type u) :
Type (u+1)

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

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} (w : 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} (w : ∀ {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} (w : ∀ {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) (w : (λ {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) (w : (λ {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) (w : ∀ {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) (w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) :
f = 𝟙 X
source
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')
source
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)
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} (f : 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.

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

Instances of this typeclass
source
@[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 ≫ f → g = 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 of this typeclass
source
@[protected, instance]
def category_theory.category_struct.id.epi {C : Type u} [category_theory.category C] (X : C) :
category_theory.epi (𝟙 X)
source
@[protected, instance]
def category_theory.category_struct.id.mono {C : Type u} [category_theory.category C] (X : C) :
category_theory.mono (𝟙 X)
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
@[instance]
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] (w : 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] (w : f ≫ g = h) :
category_theory.epi g
source
@[protected, instance]
def category_theory.ulift_category (C : Type u) [category_theory.category C] :
category_theory.category (ulift C)
Equations