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.

def HomRel (C : Type u_1) [Quiver C] : Type (max u_1 u_2)

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

@[implicit_reducible]

instance instInhabitedHomRel (C : Type u_1) [Quiver C] : Inhabited (HomRel C)

def CategoryTheory.Functor.homRel {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) : HomRel C

A functor induces a HomRel on its domain, relating those maps that have the same image.

@[simp]

theorem CategoryTheory.Functor.homRel_iff {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) {X Y : C} (f g : X ⟶ Y) : F.homRel f g ↔ F.map f = F.map g

class CategoryTheory.HomRel.IsStableUnderPrecomp {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : Prop

The condition that a HomRel is stable under precomposition.

• comp_left {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z} : r g g' → r (CategoryStruct.comp f g) (CategoryStruct.comp f g')

class CategoryTheory.HomRel.IsStableUnderPostcomp {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : Prop

The condition that a HomRel is stable under postcomposition.

• comp_right {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z) : r f f' → r (CategoryStruct.comp f g) (CategoryStruct.comp f' g)

inductive CategoryTheory.HomRel.CompClosure {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : HomRel C

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

• intro {C : Type u_1} [Category.{v_1, u_1} C] {r : HomRel C} {s t : C} (a b : C) (f : s ⟶ a) (m₁ m₂ : a ⟶ b) (g : b ⟶ t) (h : r m₁ m₂) : CompClosure r (CategoryStruct.comp f (CategoryStruct.comp m₁ g)) (CategoryStruct.comp f (CategoryStruct.comp m₂ g))

theorem CategoryTheory.HomRel.CompClosure.of {C : Type u_1} [Category.{v_1, u_1} C] {r : HomRel C} {a b : C} {m₁ m₂ : a ⟶ b} (h : r m₁ m₂) : CompClosure r m₁ m₂

instance CategoryTheory.HomRel.instIsStableUnderPrecompCompClosure {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : IsStableUnderPrecomp (CompClosure r)

instance CategoryTheory.HomRel.instIsStableUnderPostcompCompClosure {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : IsStableUnderPostcomp (CompClosure r)

theorem CategoryTheory.HomRel.compClosure_iff_self {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [IsStableUnderPrecomp r] [IsStableUnderPostcomp r] {X Y : C} (f g : X ⟶ Y) : CompClosure r f g ↔ r f g

@[simp]

theorem CategoryTheory.HomRel.compClosure_eq_self {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [IsStableUnderPrecomp r] [IsStableUnderPostcomp r] : CompClosure r = r

class CategoryTheory.Congruence {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) extends CategoryTheory.HomRel.IsStableUnderPrecomp r, CategoryTheory.HomRel.IsStableUnderPostcomp r : Prop

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

• comp_left {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z} : r g g' → r (CategoryStruct.comp f g) (CategoryStruct.comp f g')
• comp_right {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z) : r f f' → r (CategoryStruct.comp f g) (CategoryStruct.comp f' g)
• equivalence {X Y : C} : _root_.Equivalence r

  r is an equivalence on every hom-set.

@[deprecated CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left (since := "2025-12-23")]

theorem CategoryTheory.Congruence.compLeft {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {r : HomRel C} [self : HomRel.IsStableUnderPrecomp r] {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z} : r g g' → r (CategoryStruct.comp f g) (CategoryStruct.comp f g')

Alias of CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left.

@[deprecated CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right (since := "2025-12-23")]

theorem CategoryTheory.Congruence.compRight {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {r : HomRel C} [self : HomRel.IsStableUnderPostcomp r] {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z) : r f f' → r (CategoryStruct.comp f g) (CategoryStruct.comp f' g)

Alias of CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right.

instance CategoryTheory.Functor.congruence_homRel {C : Type u_2} {D : Type u_3} [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] (F : Functor C D) : Congruence F.homRel

For F : C ⥤ D, F.homRel is a congruence.

structure CategoryTheory.Quotient {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : Type u_1

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

• as : C

  The object of C.

theorem CategoryTheory.Quotient.ext {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {r : HomRel C} {x y : Quotient r} (as : x.as = y.as) : x = y

theorem CategoryTheory.Quotient.ext_iff {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {r : HomRel C} {x y : Quotient r} : x = y ↔ x.as = y.as

@[implicit_reducible]

instance CategoryTheory.instInhabitedQuotient {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [Inhabited C] : Inhabited (Quotient r)

@[deprecated CategoryTheory.HomRel.CompClosure (since := "2025-12-23")]

def CategoryTheory.Quotient.CompClosure {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : HomRel C

Alias of CategoryTheory.HomRel.CompClosure.

---

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

@[deprecated CategoryTheory.HomRel.CompClosure.of (since := "2025-12-23")]

theorem CategoryTheory.Quotient.CompClosure.of {C : Type u_1} [Category.{v_1, u_1} C] {r : HomRel C} {a b : C} {m₁ m₂ : a ⟶ b} (h : r m₁ m₂) : HomRel.CompClosure r m₁ m₂

Alias of CategoryTheory.HomRel.CompClosure.of.

@[deprecated CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left (since := "2025-12-23")]

theorem CategoryTheory.Quotient.comp_left {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {r : HomRel C} [self : HomRel.IsStableUnderPrecomp r] {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z} : r g g' → r (CategoryStruct.comp f g) (CategoryStruct.comp f g')

Alias of CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left.

@[deprecated CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right (since := "2025-12-23")]

theorem CategoryTheory.Quotient.comp_right {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {r : HomRel C} [self : HomRel.IsStableUnderPostcomp r] {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z) : r f f' → r (CategoryStruct.comp f g) (CategoryStruct.comp f' g)

Alias of CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right.

@[deprecated CategoryTheory.HomRel.compClosure_iff_self (since := "2025-12-23")]

theorem CategoryTheory.Quotient.compClosure_iff_self {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [HomRel.IsStableUnderPrecomp r] [HomRel.IsStableUnderPostcomp r] {X Y : C} (f g : X ⟶ Y) : HomRel.CompClosure r f g ↔ r f g

Alias of CategoryTheory.HomRel.compClosure_iff_self.

@[deprecated CategoryTheory.HomRel.compClosure_eq_self (since := "2025-12-23")]

theorem CategoryTheory.Quotient.compClosure_eq_self {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [HomRel.IsStableUnderPrecomp r] [HomRel.IsStableUnderPostcomp r] : HomRel.CompClosure r = r

Alias of CategoryTheory.HomRel.compClosure_eq_self.

def CategoryTheory.Quotient.Hom {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) (s t : Quotient r) : Type v_1

Hom-sets of the quotient category.

@[implicit_reducible]

instance CategoryTheory.Quotient.instInhabitedHom {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) (a : Quotient r) : Inhabited (Hom r a a)

def CategoryTheory.Quotient.comp {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) ⦃a b c : Quotient r⦄ : Hom r a b → Hom r b c → Hom r a c

Composition in the quotient category.

@[simp]

theorem CategoryTheory.Quotient.comp_mk {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {a b c : Quotient r} (f : a.as ⟶ b.as) (g : b.as ⟶ c.as) : comp r (Quot.mk (HomRel.CompClosure r) f) (Quot.mk (HomRel.CompClosure r) g) = Quot.mk (HomRel.CompClosure r) (CategoryStruct.comp f g)

@[implicit_reducible]

instance CategoryTheory.Quotient.category {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : Category.{v_1, u_1} (Quotient r)

def CategoryTheory.Quotient.equiv {C : Type u_2} [Category.{v_2, u_2} C] (r : HomRel C) : Quotient r ≃ C

An equivalence between the type synonym for a quotient category and the type alias for the original category.

def CategoryTheory.Quotient.inv {G : Type u_2} [Groupoid G] (r : HomRel G) {X Y : Quotient r} (f : X ⟶ Y) : Y ⟶ X

Inverse of a map in the quotient category of a groupoid.

@[simp]

theorem CategoryTheory.Quotient.inv_mk {G : Type u_2} [Groupoid G] (r : HomRel G) {X Y : Quotient r} (f : X.as ⟶ Y.as) : Quotient.inv r (Quot.mk (HomRel.CompClosure r) f) = Quot.mk (HomRel.CompClosure r) (Groupoid.inv f)

@[implicit_reducible]

instance CategoryTheory.Quotient.groupoid {G : Type u_2} [Groupoid G] (r : HomRel G) : Groupoid (Quotient r)

The quotient of a groupoid is a groupoid.

def CategoryTheory.Quotient.functor {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : Functor C (Quotient r)

The functor from a category to its quotient.

instance CategoryTheory.Quotient.full_functor {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : (functor r).Full

instance CategoryTheory.Quotient.essSurj_functor {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : (functor r).EssSurj

@[implicit_reducible]

instance CategoryTheory.Quotient.instUnique {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [Unique C] : Unique (Quotient r)

instance CategoryTheory.Quotient.instSubsingletonHom {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [∀ (x y : C), Subsingleton (x ⟶ y)] (x y : Quotient r) : Subsingleton (x ⟶ y)

theorem CategoryTheory.Quotient.induction {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {P : {a b : Quotient r} → (a ⟶ b) → Prop} (h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)) {a b : Quotient r} (f : a ⟶ b) : P f

theorem CategoryTheory.Quotient.sound {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {a b : C} {f₁ f₂ : a ⟶ b} (h : r f₁ f₂) : (functor r).map f₁ = (functor r).map f₂

theorem CategoryTheory.Quotient.functor_map_eq_iff {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [h : Congruence r] {X Y : C} (f f' : X ⟶ Y) : (functor r).map f = (functor r).map f' ↔ r f f'

theorem CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {X Y : C} (f g : X ⟶ Y) : (functor r).homRel f g ↔ Relation.EqvGen (HomRel.CompClosure r) f g

theorem CategoryTheory.Quotient.compClosure.congruence {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) : Congruence fun (X Y : C) => Relation.EqvGen (HomRel.CompClosure r)

def CategoryTheory.Quotient.lift {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) : Functor (Quotient r) D

The induced functor on the quotient category.

theorem CategoryTheory.Quotient.lift_spec {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) : (functor r).comp (lift r F H) = F

theorem CategoryTheory.Quotient.lift_unique {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (Φ : Functor (Quotient r) D) (hΦ : (functor r).comp Φ = F) : Φ = lift r F H

theorem CategoryTheory.Quotient.lift_unique' {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F₁ F₂ : Functor (Quotient r) D) (h : (functor r).comp F₁ = (functor r).comp F₂) : F₁ = F₂

def CategoryTheory.Quotient.lift.isLift {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) : (functor r).comp (lift r F H) ≅ F

The original functor factors through the induced functor.

@[simp]

theorem CategoryTheory.Quotient.lift.isLift_hom {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (X : C) : (isLift r F H).hom.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Quotient.lift.isLift_inv {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (X : C) : (isLift r F H).inv.app X = CategoryStruct.id (F.obj X)

theorem CategoryTheory.Quotient.lift_obj_functor_obj {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (X : C) : (lift r F H).obj ((functor r).obj X) = F.obj X

theorem CategoryTheory.Quotient.lift_map_functor_map {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor 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) : (lift r F H).map ((functor r).map f) = F.map f

theorem CategoryTheory.Quotient.natTrans_ext {C : Type u_1} [Category.{v_1, u_1} C] {r : HomRel C} {D : Type u_2} [Category.{v_2, u_2} D] {F G : Functor (Quotient r) D} (τ₁ τ₂ : F ⟶ G) (h : (functor r).whiskerLeft τ₁ = (functor r).whiskerLeft τ₂) : τ₁ = τ₂

def CategoryTheory.Quotient.natTransLift {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] {F G : Functor (Quotient r) D} (τ : (functor r).comp F ⟶ (functor r).comp G) : F ⟶ G

In order to define a natural transformation F ⟶ G with F G : Quotient r ⥤ D, it suffices to do so after precomposing with Quotient.functor r.

@[simp]

theorem CategoryTheory.Quotient.natTransLift_app {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F G : Functor (Quotient r) D) (τ : (functor r).comp F ⟶ (functor r).comp G) (X : C) : (natTransLift r τ).app ((functor r).obj X) = τ.app X

theorem CategoryTheory.Quotient.comp_natTransLift {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] {F G H : Functor (Quotient r) D} (τ : (functor r).comp F ⟶ (functor r).comp G) (τ' : (functor r).comp G ⟶ (functor r).comp H) : CategoryStruct.comp (natTransLift r τ) (natTransLift r τ') = natTransLift r (CategoryStruct.comp τ τ')

theorem CategoryTheory.Quotient.comp_natTransLift_assoc {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] {F G H : Functor (Quotient r) D} (τ : (functor r).comp F ⟶ (functor r).comp G) (τ' : (functor r).comp G ⟶ (functor r).comp H) {Z : Functor (Quotient r) D} (h : H ⟶ Z) : CategoryStruct.comp (natTransLift r τ) (CategoryStruct.comp (natTransLift r τ') h) = CategoryStruct.comp (natTransLift r (CategoryStruct.comp τ τ')) h

@[simp]

theorem CategoryTheory.Quotient.natTransLift_id {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor (Quotient r) D) : natTransLift r (CategoryStruct.id ((functor r).comp F)) = CategoryStruct.id F

def CategoryTheory.Quotient.natIsoLift {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] {F G : Functor (Quotient r) D} (τ : (functor r).comp F ≅ (functor r).comp G) : F ≅ G

In order to define a natural isomorphism F ≅ G with F G : Quotient r ⥤ D, it suffices to do so after precomposing with Quotient.functor r.

@[simp]

theorem CategoryTheory.Quotient.natIsoLift_hom {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] {F G : Functor (Quotient r) D} (τ : (functor r).comp F ≅ (functor r).comp G) : (natIsoLift r τ).hom = natTransLift r τ.hom

@[simp]

theorem CategoryTheory.Quotient.natIsoLift_inv {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2} [Category.{v_2, u_2} D] {F G : Functor (Quotient r) D} (τ : (functor r).comp F ≅ (functor r).comp G) : (natIsoLift r τ).inv = natTransLift r τ.inv

instance CategoryTheory.Quotient.full_whiskeringLeft_functor {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) (D : Type u_2) [Category.{v_2, u_2} D] : ((Functor.whiskeringLeft C (Quotient r) D).obj (functor r)).Full

instance CategoryTheory.Quotient.faithful_whiskeringLeft_functor {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) (D : Type u_2) [Category.{v_2, u_2} D] : ((Functor.whiskeringLeft C (Quotient r) D).obj (functor r)).Faithful