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

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

    Instances

      r is an equivalence on every hom-set.

      theorem CategoryTheory.Congruence.compLeft {C : Type u_1} :
      ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {r : HomRel C} [self : CategoryTheory.Congruence r] {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.

      theorem CategoryTheory.Congruence.compRight {C : Type u_1} :
      ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {r : HomRel C} [self : CategoryTheory.Congruence r] {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.

      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.asx = y
      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

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

      • as : C

        The object of C.

      Instances For
        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

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

        Instances For
          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 m₁ m₂) :

          Composition in the quotient category.

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

            The functor from a category to its quotient.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              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).map f)) {a : CategoryTheory.Quotient r} {b : CategoryTheory.Quotient r} (f : a b) :
              P 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 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 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} [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 f₁ f₂F.map f₁ = F.map 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 f₁ f₂F.map f₁ = F.map f₂) (Φ : CategoryTheory.Functor (CategoryTheory.Quotient r) D) (hΦ : (CategoryTheory.Quotient.functor r).comp Φ = F) :
                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 f₁ f₂F.map f₁ = F.map 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} [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 f₁ f₂F.map f₁ = F.map f₂) (X : C) :
                  @[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 f₁ f₂F.map f₁ = F.map f₂) (X : C) :
                  theorem CategoryTheory.Quotient.lift_obj_functor_obj {C : Type u_4} [CategoryTheory.Category.{u_2, u_4} C] (r : HomRel C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] (F : CategoryTheory.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_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 f₁ f₂F.map f₁ = F.map f₂) {X : C} {Y : C} (f : X Y) :

                  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
                  Instances For

                    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
                    Instances For