mathlibdocumentation

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.

@[protected, 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
• = Π ⦃X Y : C⦄, (X Y)(X Y) → Prop
@[class]
structure category_theory.congruence {C : Type u_1} (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} (r : hom_rel C) :
Type u_1
• as : C

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

@[protected, instance]
def category_theory.quotient.inhabited {C : Type u_1} (r : hom_rel C) [inhabited C] :
Equations
inductive category_theory.quotient.comp_closure {C : Type u_1} (r : hom_rel C) ⦃s t : C⦄ :
(s t)(s t) → Prop
• intro : ∀ {C : Type u_1} [_inst_1 : {r : hom_rel C} ⦃s t : C⦄ {a b : C} (f : s a) (m₁ m₂ : a b) (g : b t), r m₁ m₂ (f m₁ g) (f m₂ g)

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} (r : hom_rel C) {a b c : C} (f : a b) (g₁ g₂ : b c) (h : g₂) :
(f g₂)
theorem category_theory.quotient.comp_right {C : Type u_1} (r : hom_rel C) {a b c : C} (g : b c) (f₁ f₂ : a b) (h : f₂) :
(f₂ g)
def category_theory.quotient.hom {C : Type u_1} (r : hom_rel C) (s t : category_theory.quotient r) :
Type u_2

Hom-sets of the quotient category.

Equations
@[protected, instance]
Equations
def category_theory.quotient.comp {C : Type u_1} (r : hom_rel C) ⦃a b c : category_theory.quotient r⦄ :

Composition in the quotient category.

Equations
• = λ (hf : (hg : , (λ (f : a.as b.as), (λ (g : b.as c.as), quot.mk (f g)) _) _
@[simp]
theorem category_theory.quotient.comp_mk {C : Type u_1} (r : hom_rel C) {a b c : category_theory.quotient r} (f : a.as b.as) (g : b.as c.as) :
(quot.mk f) (quot.mk g) = quot.mk (f g)
@[protected, instance]
def category_theory.quotient.category {C : Type u_1} (r : hom_rel C) :
Equations
def category_theory.quotient.functor {C : Type u_1} (r : hom_rel C) :

The functor from a category to its quotient.

Equations
@[simp]
theorem category_theory.quotient.functor_map {C : Type u_1} (r : hom_rel C) (_x _x_1 : C) (f : _x _x_1) :
= quot.mk f
@[simp]
theorem category_theory.quotient.functor_obj_as {C : Type u_1} (r : hom_rel C) (a : C) :
.as = a
@[protected, instance]
noncomputable def category_theory.quotient.functor.category_theory.full {C : Type u_1} (r : hom_rel C) :
Equations
@[protected, instance]
@[protected]
theorem category_theory.quotient.induction {C : Type u_1} (r : hom_rel C) {P : Π {a b : , (a b) → Prop} (h : ∀ {x y : C} (f : x y), P ) {a b : category_theory.quotient r} (f : a b) :
P f
@[protected]
theorem category_theory.quotient.sound {C : Type u_1} (r : hom_rel C) {a b : C} {f₁ f₂ : a b} (h : r f₁ f₂) :
theorem category_theory.quotient.functor_map_eq_iff {C : Type u_1} (r : hom_rel C) {X Y : C} (f f' : X Y) :
r f f'
@[simp]
theorem category_theory.quotient.lift_map {C : Type u_1} (r : hom_rel C) {D : Type u_3} (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) :
.map hf = (λ (f : a.as b.as), F.map f) _
@[simp]
theorem category_theory.quotient.lift_obj {C : Type u_1} (r : hom_rel C) {D : Type u_3} (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) :
.obj a = F.obj a.as
def category_theory.quotient.lift {C : Type u_1} (r : hom_rel C) {D : Type u_3} (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} (r : hom_rel C) {D : Type u_3} (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} (r : hom_rel C) {D : Type u_3} (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (X : C) :
X = 𝟙 (F.obj X)
@[simp]
theorem category_theory.quotient.lift.is_lift_inv {C : Type u_1} (r : hom_rel C) {D : Type u_3} (F : C D) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (X : C) :
X = 𝟙 (F.obj X)
theorem category_theory.quotient.lift_map_functor_map {C : Type u_1} (r : hom_rel C) {D : Type u_3} (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) :
.map = F.map f