mathlib3 documentation

category_theory.quotient

Quotient category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
Instances for hom_rel
@[class]
structure category_theory.congruence {C : Type u_1} [category_theory.category C] (r : hom_rel C) :
Prop

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 of this typeclass
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.

Instances for category_theory.quotient
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_closure.of {C : Type u_1} [category_theory.category C] (r : hom_rel C) {a b : C} (m₁ m₂ : a b) (h : r m₁ m₂) :
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₂) :

Hom-sets of the quotient category.

Equations
Instances for category_theory.quotient.hom

The functor from a category to its quotient.

Equations
Instances for category_theory.quotient.functor
@[protected]
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
@[protected]
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
theorem category_theory.quotient.lift_spec {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₂) :
theorem category_theory.quotient.lift_unique {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₂) (Φ : category_theory.quotient r D) (hΦ : category_theory.quotient.functor r Φ = F) :
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) :