mathlib documentation

category_theory.quotient

Quotient category #

Constructs the quotient of a category by an arbitrary family of relations on its hom-sets, by introducing a type synonym for the objects, and identifying homs as necessary.

This is analogous to 'the quotient of a group by the normal closure of a subset', rather than 'the quotient of a group by a normal subgroup'. When taking the quotient by a congruence relation, functor_map_eq_iff says that no unnecessary identifications have been made.

@[instance]
def hom_rel.inhabited (C : Type u_1) [quiver C] :
def hom_rel (C : Type u_1) [quiver C] :
Sort (max (u_1+1) u_2 1)

A hom_rel on C consists of a relation on every hom-set.

Equations
@[class]
structure category_theory.congruence {C : Type u_1} [category_theory.category C] (r : hom_rel C) :
Prop
  • is_equiv : ∀ {X Y : C}, is_equiv (X Y) r
  • comp_left : ∀ {X Y Z : C} (f : X Y) {g g' : Y Z}, r g g'r (f g) (f g')
  • comp_right : ∀ {X Y Z : C} {f f' : X Y} (g : Y Z), r f f'r (f g) (f' g)

A hom_rel is a congruence when it's an equivalence on every hom-set, and it can be composed from left and right.

Instances
theorem category_theory.quotient.ext_iff {C : Type u_1} {_inst_1 : category_theory.category C} {r : hom_rel C} (x y : category_theory.quotient r) :
x = y x.as = y.as
theorem category_theory.quotient.ext {C : Type u_1} {_inst_1 : category_theory.category C} {r : hom_rel C} (x y : category_theory.quotient r) (h : x.as = y.as) :
x = y
@[ext]
structure category_theory.quotient {C : Type u_1} [category_theory.category C] (r : hom_rel C) :
Type u_1
  • as : C

A type synonym for C, thought of as the objects of the quotient category.

inductive category_theory.quotient.comp_closure {C : Type u_1} [category_theory.category C] (r : hom_rel C) ⦃s t : C⦄ :
(s t)(s t) → Prop

Generates the closure of a family of relations w.r.t. composition from left and right.

theorem category_theory.quotient.comp_left {C : Type u_1} [category_theory.category C] (r : hom_rel C) {a b c : C} (f : a b) (g₁ g₂ : b c) (h : category_theory.quotient.comp_closure r g₁ g₂) :
theorem category_theory.quotient.comp_right {C : Type u_1} [category_theory.category C] (r : hom_rel C) {a b c : C} (g : b c) (f₁ f₂ : a b) (h : category_theory.quotient.comp_closure r f₁ f₂) :
def category_theory.quotient.hom {C : Type u_1} [category_theory.category C] (r : hom_rel C) (s t : category_theory.quotient r) :
Type u_2

Hom-sets of the quotient category.

Equations

Composition in the quotient category.

Equations

The functor from a category to its quotient.

Equations
@[simp]
theorem category_theory.quotient.induction {C : Type u_1} [category_theory.category C] (r : hom_rel C) {P : Π {a b : category_theory.quotient r}, (a b) → Prop} (h : ∀ {x y : C} (f : x y), P ((category_theory.quotient.functor r).map f)) {a b : category_theory.quotient r} (f : a b) :
P f
theorem category_theory.quotient.sound {C : Type u_1} [category_theory.category C] (r : hom_rel C) {a b : C} {f₁ f₂ : a b} (h : r f₁ f₂) :
@[simp]
theorem category_theory.quotient.lift_map {C : Type u_1} [category_theory.category C] (r : hom_rel C) {D : Type u_3} [category_theory.category D] (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (a b : category_theory.quotient r) (hf : a b) :
(category_theory.quotient.lift r F H).map hf = quot.lift_on hf (λ (f : a.as b.as), F.map f) _
@[simp]
theorem category_theory.quotient.lift_obj {C : Type u_1} [category_theory.category C] (r : hom_rel C) {D : Type u_3} [category_theory.category D] (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (a : category_theory.quotient r) :
def category_theory.quotient.lift {C : Type u_1} [category_theory.category C] (r : hom_rel C) {D : Type u_3} [category_theory.category D] (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) :

The induced functor on the quotient category.

Equations
def category_theory.quotient.lift.is_lift {C : Type u_1} [category_theory.category C] (r : hom_rel C) {D : Type u_3} [category_theory.category D] (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) :

The original functor factors through the induced functor.

Equations
@[simp]
theorem category_theory.quotient.lift.is_lift_hom {C : Type u_1} [category_theory.category C] (r : hom_rel C) {D : Type u_3} [category_theory.category D] (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (X : C) :
@[simp]
theorem category_theory.quotient.lift.is_lift_inv {C : Type u_1} [category_theory.category C] (r : hom_rel C) {D : Type u_3} [category_theory.category D] (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (X : C) :
theorem category_theory.quotient.lift_map_functor_map {C : Type u_1} [category_theory.category C] (r : hom_rel C) {D : Type u_3} [category_theory.category D] (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) {X Y : C} (f : X Y) :