Theorems · Definition · category theory

CategoryTheory.Quotient.lift

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            (∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) →
              CategoryTheory.Functor (CategoryTheory.Quotient r) D

The induced functor on the quotient category.

Defined in

Mathlib.CategoryTheory.Quotient

Cited by

11 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category