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] : Sort (max (u_1 + 1) u_2)

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

Equations

• HomRel C = (⦃X Y : C⦄ → (X ⟶ Y) → (X ⟶ Y) → Prop)

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

Equations

• instInhabitedHomRel C = { default := fun x x_1 x_2 x => PUnit.{0} }

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

• equivalence : ∀ {X Y : C}, Equivalence r

  r is an equivalence on every hom-set.

• compLeft : ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, r g g' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g')

  Precomposition with an arrow respects r.

• compRight : ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z), r f f' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g)

  Postcomposition with an arrow respects r.

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

theorem CategoryTheory.Quotient.ext_iff {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {r : HomRel C} (x y : CategoryTheory.Quotient r), x = y ↔ x.as = y.as

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

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

• as : C

  The object of C.

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

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

Equations

• CategoryTheory.instInhabitedQuotient r = { default := { as := default } }

inductive CategoryTheory.Quotient.CompClosure {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r : HomRel C) ⦃s : C⦄ ⦃t : C⦄ : (s ⟶ t) → (s ⟶ t) → Prop

• intro: ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {r : HomRel C} ⦃s t : C⦄ {a b : C} (f : s ⟶ a) (m₁ m₂ : a ⟶ b) (g : b ⟶ t), r m₁ m₂ → CategoryTheory.Quotient.CompClosure r (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp m₁ g)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp m₂ g))

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

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

theorem CategoryTheory.Quotient.comp_left {C : Type u_2} [CategoryTheory.Category.{u_1, u_2} C] (r : HomRel C) {a : C} {b : C} {c : C} (f : a ⟶ b) (g₁ : b ⟶ c) (g₂ : b ⟶ c) : CategoryTheory.Quotient.CompClosure r g₁ g₂ → CategoryTheory.Quotient.CompClosure r (CategoryTheory.CategoryStruct.comp f g₁) (CategoryTheory.CategoryStruct.comp f g₂)

theorem CategoryTheory.Quotient.comp_right {C : Type u_2} [CategoryTheory.Category.{u_1, u_2} C] (r : HomRel C) {a : C} {b : C} {c : C} (g : b ⟶ c) (f₁ : a ⟶ b) (f₂ : a ⟶ b) : CategoryTheory.Quotient.CompClosure r f₁ f₂ → CategoryTheory.Quotient.CompClosure r (CategoryTheory.CategoryStruct.comp f₁ g) (CategoryTheory.CategoryStruct.comp f₂ g)

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

Hom-sets of the quotient category.

Equations

• CategoryTheory.Quotient.Hom r s t = Quot (CategoryTheory.Quotient.CompClosure r)

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

Equations

• CategoryTheory.Quotient.instInhabitedHom r a = { default := Quot.mk (CategoryTheory.Quotient.CompClosure r) (CategoryTheory.CategoryStruct.id a.as) }

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

Composition in the quotient category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• CategoryTheory.Quotient.category r = CategoryTheory.Category.mk

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

The functor from a category to its quotient.

Equations

• CategoryTheory.Quotient.functor r = CategoryTheory.Functor.mk { obj := fun a => { as := a }, map := fun x x_1 f => Quot.mk (CategoryTheory.Quotient.CompClosure r) f }

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

Equations

• CategoryTheory.Quotient.fullFunctor r = CategoryTheory.Full.mk fun X Y f => Quot.out f

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

Equations

• @CategoryTheory.Quotient.instEssSurjQuotientCategoryFunctor = @CategoryTheory.Quotient.instEssSurjQuotientCategoryFunctor.proof_1

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

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

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

@[simp]

theorem CategoryTheory.Quotient.compClosure_eq_self {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r : HomRel C) [h : CategoryTheory.Congruence r] : CategoryTheory.Quotient.CompClosure r = r

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

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

The induced functor on the quotient category.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

The original functor factors through the induced functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

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

def CategoryTheory.Quotient.natTransLift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] {F : CategoryTheory.Functor (CategoryTheory.Quotient r) D} {G : CategoryTheory.Functor (CategoryTheory.Quotient r) D} (τ : CategoryTheory.Functor.comp (CategoryTheory.Quotient.functor r) F ⟶ CategoryTheory.Functor.comp (CategoryTheory.Quotient.functor r) 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.

Equations

• CategoryTheory.Quotient.natTransLift r τ = CategoryTheory.NatTrans.mk fun x => match x with | { as := X } => τ.app X

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Quotient.natIsoLift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] {F : CategoryTheory.Functor (CategoryTheory.Quotient r) D} {G : CategoryTheory.Functor (CategoryTheory.Quotient r) D} (τ : CategoryTheory.Functor.comp (CategoryTheory.Quotient.functor r) F ≅ CategoryTheory.Functor.comp (CategoryTheory.Quotient.functor r) 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.

Equations

• CategoryTheory.Quotient.natIsoLift r τ = CategoryTheory.Iso.mk (CategoryTheory.Quotient.natTransLift r τ.hom) (CategoryTheory.Quotient.natTransLift r τ.inv)

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

Equations

• CategoryTheory.Quotient.full_whiskeringLeft_functor r D = CategoryTheory.Full.mk fun {X Y} => CategoryTheory.Quotient.natTransLift r

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

Equations

• @CategoryTheory.Quotient.faithful_whiskeringLeft_functor = @CategoryTheory.Quotient.faithful_whiskeringLeft_functor.proof_1