Documentation

Mathlib.CategoryTheory.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.

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
instance instInhabitedHomRel (C : Type u_1) [Quiver C] :
Equations

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

Equations
@[simp]
theorem CategoryTheory.Functor.homRel_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {X Y : C} (f g : X Y) :
F.homRel f g F.map f = F.map g

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

Instances

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

    structure CategoryTheory.Quotient {C : Type u_1} [Category.{u_2, 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.{u_2, 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.{u_2, u_1} C} {r : HomRel C} {x y : Quotient r} :
    x = y x.as = y.as
    inductive CategoryTheory.Quotient.CompClosure {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel 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 CategoryTheory.Quotient.CompClosure.of {C : Type u_2} [Category.{u_1, u_2} C] (r : HomRel C) {a b : C} (m₁ m₂ : a b) (h : r m₁ m₂) :
    CompClosure r m₁ m₂
    theorem CategoryTheory.Quotient.comp_left {C : Type u_2} [Category.{u_1, u_2} C] (r : HomRel C) {a b c : C} (f : a b) (g₁ g₂ : b c) :
    theorem CategoryTheory.Quotient.comp_right {C : Type u_2} [Category.{u_1, u_2} C] (r : HomRel C) {a b c : C} (g : b c) (f₁ f₂ : a b) :
    def CategoryTheory.Quotient.Hom {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) (s t : Quotient r) :
    Type u_2

    Hom-sets of the quotient category.

    Equations
    def CategoryTheory.Quotient.comp {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) a b c : Quotient r :
    Hom r a bHom r b cHom 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} [Category.{u_2, u_1} C] (r : HomRel C) {a b c : Quotient r} (f : a.as b.as) (g : b.as c.as) :
    Equations
    • One or more equations did not get rendered due to their size.

    The functor from a category to its quotient.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem CategoryTheory.Quotient.induction {C : Type u_1} [Category.{u_2, 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_2} [Category.{u_1, u_2} 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.compClosure_iff_self {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) [h : Congruence r] {X Y : C} (f g : X Y) :
    CompClosure r f g r f g
    theorem CategoryTheory.Quotient.functor_map_eq_iff {C : Type u_1} [Category.{u_2, 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'
    def CategoryTheory.Quotient.lift {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [Category.{u_4, u_3} D] (F : Functor 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
    • One or more equations did not get rendered due to their size.
    theorem CategoryTheory.Quotient.lift_spec {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [Category.{u_4, u_3} 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_3} [Category.{u_1, u_3} C] (r : HomRel C) {D : Type u_4} [Category.{u_2, u_4} 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) ( : (functor r).comp Φ = F) :
    Φ = lift r F H
    theorem CategoryTheory.Quotient.lift_unique' {C : Type u_3} [Category.{u_1, u_3} C] (r : HomRel C) {D : Type u_4} [Category.{u_2, u_4} 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.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [Category.{u_4, u_3} 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.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CategoryTheory.Quotient.lift.isLift_hom {C : Type u_4} [Category.{u_3, u_4} C] (r : HomRel C) {D : Type u_2} [Category.{u_1, 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) :
    @[simp]
    theorem CategoryTheory.Quotient.lift.isLift_inv {C : Type u_4} [Category.{u_3, u_4} C] (r : HomRel C) {D : Type u_2} [Category.{u_1, 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) :
    theorem CategoryTheory.Quotient.lift_obj_functor_obj {C : Type u_4} [Category.{u_2, u_4} C] (r : HomRel C) {D : Type u_1} [Category.{u_3, u_1} 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_2} [Category.{u_1, u_2} C] (r : HomRel C) {D : Type u_4} [Category.{u_3, u_4} 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_3} [Category.{u_1, u_3} C] {r : HomRel C} {D : Type u_4} [Category.{u_2, u_4} D] {F G : Functor (Quotient r) D} (τ₁ τ₂ : F G) (h : whiskerLeft (functor r) τ₁ = whiskerLeft (functor r) τ₂) :
    τ₁ = τ₂
    def CategoryTheory.Quotient.natTransLift {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [Category.{u_4, u_3} 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.

    Equations
    @[simp]
    theorem CategoryTheory.Quotient.natTransLift_app {C : Type u_3} [Category.{u_1, u_3} C] (r : HomRel C) {D : Type u_4} [Category.{u_2, u_4} 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
    def CategoryTheory.Quotient.natIsoLift {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [Category.{u_4, u_3} 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.

    Equations
    @[simp]
    theorem CategoryTheory.Quotient.natIsoLift_inv {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [Category.{u_4, u_3} D] {F G : Functor (Quotient r) D} (τ : (functor r).comp F (functor r).comp G) :
    @[simp]
    theorem CategoryTheory.Quotient.natIsoLift_hom {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) {D : Type u_3} [Category.{u_4, u_3} D] {F G : Functor (Quotient r) D} (τ : (functor r).comp F (functor r).comp G) :