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

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

Equations
• = (X Y : C⦄ → (X Y)(X Y)Prop)
Instances For
instance instInhabitedHomRel (C : Type u_1) [] :
Equations
• = { default := fun (x x_1 : C) (x_2 x : x x_1) => PUnit.{0} }
class CategoryTheory.Congruence {C : Type u_1} [] (r : ) :

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

• equivalence : ∀ {X Y : C},

r is an equivalence on every hom-set.

• compLeft : ∀ {X Y Z : C} (f : X Y) {g g' : Y Z}, r g g'

Precomposition with an arrow respects r.

• compRight : ∀ {X Y Z : C} {f f' : X Y} (g : Y Z), r f f'

Postcomposition with an arrow respects r.

Instances
theorem CategoryTheory.Congruence.equivalence {C : Type u_1} [] {r : } [self : ] {X : C} {Y : C} :

r is an equivalence on every hom-set.

theorem CategoryTheory.Congruence.compLeft {C : Type u_1} [] {r : } [self : ] {X : C} {Y : C} {Z : C} (f : X Y) {g : Y Z} {g' : Y Z} :
r g g'

Precomposition with an arrow respects r.

theorem CategoryTheory.Congruence.compRight {C : Type u_1} [] {r : } [self : ] {X : C} {Y : C} {Z : C} {f : X Y} {f' : X Y} (g : Y Z) :
r f f'

Postcomposition with an arrow respects r.

theorem CategoryTheory.Quotient.ext {C : Type u_1} :
∀ {inst : } {r : } (x y : ), x.as = y.asx = y
theorem CategoryTheory.Quotient.ext_iff {C : Type u_1} :
∀ {inst : } {r : } (x y : ), x = y x.as = y.as
structure CategoryTheory.Quotient {C : Type u_1} [] (r : ) :
Type u_1

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

• as : C

The object of C.

Instances For
instance CategoryTheory.instInhabitedQuotient {C : Type u_1} [] (r : ) [] :
Equations
• = { default := { as := default } }
inductive CategoryTheory.Quotient.CompClosure {C : Type u_1} [] (r : ) ⦃s : C ⦃t : C :
(s t)(s t)Prop

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

• intro: ∀ {C : Type u_1} [inst : ] {r : } ⦃s t : C⦄ {a b : C} (f : s a) (m₁ m₂ : a b) (g : b t), r m₁ m₂
Instances For
theorem CategoryTheory.Quotient.CompClosure.of {C : Type u_2} [] (r : ) {a : C} {b : C} (m₁ : a b) (m₂ : a b) (h : r m₁ m₂) :
theorem CategoryTheory.Quotient.comp_left {C : Type u_2} [] (r : ) {a : C} {b : C} {c : C} (f : a b) (g₁ : b c) (g₂ : b c) :
theorem CategoryTheory.Quotient.comp_right {C : Type u_2} [] (r : ) {a : C} {b : C} {c : C} (g : b c) (f₁ : a b) (f₂ : a b) :
def CategoryTheory.Quotient.Hom {C : Type u_1} [] (r : ) (s : ) (t : ) :
Type u_2

Hom-sets of the quotient category.

Equations
Instances For
instance CategoryTheory.Quotient.instInhabitedHom {C : Type u_1} [] (r : ) (a : ) :
Equations
• = { default := }
def CategoryTheory.Quotient.comp {C : Type u_1} [] (r : ) ⦃a : ⦃b : ⦃c : :

Composition in the quotient category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Quotient.comp_mk {C : Type u_1} [] (r : ) {a : } {b : } {c : } (f : a.as b.as) (g : b.as c.as) :
instance CategoryTheory.Quotient.category {C : Type u_1} [] (r : ) :
Equations
def CategoryTheory.Quotient.functor {C : Type u_1} [] (r : ) :

The functor from a category to its quotient.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Quotient.full_functor {C : Type u_1} [] (r : ) :
.Full
Equations
• =
instance CategoryTheory.Quotient.essSurj_functor {C : Type u_1} [] (r : ) :
.EssSurj
Equations
• =
theorem CategoryTheory.Quotient.induction {C : Type u_1} [] (r : ) {P : {a b : } → (a b)Prop} (h : ∀ {x y : C} (f : x y), P (.map f)) {a : } {b : } (f : a b) :
P f
theorem CategoryTheory.Quotient.sound {C : Type u_2} [] (r : ) {a : C} {b : C} {f₁ : a b} {f₂ : a b} (h : r f₁ f₂) :
.map f₁ = .map f₂
theorem CategoryTheory.Quotient.compClosure_iff_self {C : Type u_1} [] (r : ) [h : ] {X : C} {Y : C} (f : X Y) (g : X Y) :
r f g
@[simp]
theorem CategoryTheory.Quotient.compClosure_eq_self {C : Type u_1} [] (r : ) [h : ] :
theorem CategoryTheory.Quotient.functor_map_eq_iff {C : Type u_1} [] (r : ) [h : ] {X : C} {Y : C} (f : X Y) (f' : X Y) :
.map f = .map f' r f f'
def CategoryTheory.Quotient.lift {C : Type u_1} [] (r : ) {D : Type u_3} [] (F : ) (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
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Quotient.lift_spec {C : Type u_1} [] (r : ) {D : Type u_3} [] (F : ) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) :
.comp () = F
theorem CategoryTheory.Quotient.lift_unique {C : Type u_3} [] (r : ) {D : Type u_4} [] (F : ) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (Φ : ) (hΦ : .comp Φ = F) :
theorem CategoryTheory.Quotient.lift_unique' {C : Type u_3} [] (r : ) {D : Type u_4} [] (F₁ : ) (F₂ : ) (h : .comp F₁ = .comp F₂) :
F₁ = F₂
def CategoryTheory.Quotient.lift.isLift {C : Type u_1} [] (r : ) {D : Type u_3} [] (F : ) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) :
.comp () F

The original functor factors through the induced functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Quotient.lift.isLift_hom {C : Type u_4} [] (r : ) {D : Type u_2} [] (F : ) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (X : C) :
.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Quotient.lift.isLift_inv {C : Type u_4} [] (r : ) {D : Type u_2} [] (F : ) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) (X : C) :
.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
theorem CategoryTheory.Quotient.lift_map_functor_map {C : Type u_2} [] (r : ) {D : Type u_4} [] (F : ) (H : ∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂) {X : C} {Y : C} (f : X Y) :
().map (.map f) = F.map f
theorem CategoryTheory.Quotient.natTrans_ext {C : Type u_3} [] {r : } {D : Type u_4} [] {F : } {G : } (τ₁ : F G) (τ₂ : F G) :
τ₁ = τ₂
def CategoryTheory.Quotient.natTransLift {C : Type u_1} [] (r : ) {D : Type u_3} [] {F : } {G : } (τ : .comp F .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.

Equations
• = { app := fun (x : ) => match x with | { as := X } => τ.app X, naturality := }
Instances For
@[simp]
theorem CategoryTheory.Quotient.natTransLift_app {C : Type u_3} [] (r : ) {D : Type u_4} [] (F : ) (G : ) (τ : .comp F .comp G) (X : C) :
.app (.obj X) = τ.app X
theorem CategoryTheory.Quotient.comp_natTransLift_assoc {C : Type u_3} [] (r : ) {D : Type u_4} [] {F : } {G : } {H : } (τ : .comp F .comp G) (τ' : .comp G .comp H) {Z : } (h : H Z) :
theorem CategoryTheory.Quotient.comp_natTransLift {C : Type u_3} [] (r : ) {D : Type u_4} [] {F : } {G : } {H : } (τ : .comp F .comp G) (τ' : .comp G .comp H) :
@[simp]
theorem CategoryTheory.Quotient.natTransLift_id {C : Type u_3} [] (r : ) {D : Type u_4} [] (F : ) :
@[simp]
theorem CategoryTheory.Quotient.natIsoLift_inv {C : Type u_1} [] (r : ) {D : Type u_3} [] {F : } {G : } (τ : .comp F .comp G) :
.inv =
@[simp]
theorem CategoryTheory.Quotient.natIsoLift_hom {C : Type u_1} [] (r : ) {D : Type u_3} [] {F : } {G : } (τ : .comp F .comp G) :
.hom =
def CategoryTheory.Quotient.natIsoLift {C : Type u_1} [] (r : ) {D : Type u_3} [] {F : } {G : } (τ : .comp F .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.

Equations
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
instance CategoryTheory.Quotient.full_whiskeringLeft_functor {C : Type u_1} [] (r : ) (D : Type u_3) [] :
().Full
Equations
• =
instance CategoryTheory.Quotient.faithful_whiskeringLeft_functor {C : Type u_1} [] (r : ) (D : Type u_3) [] :
().Faithful
Equations
• =