mathlib documentation

category_theory.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'.

structure category_theory.quotient {C : Type u} [category_theory.category C] :
(Π ⦃a b : C⦄, (a b)(a b) → Prop)Type u
  • as : C

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

@[instance]
def category_theory.inhabited {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) [inhabited C] :

Equations
inductive category_theory.quotient.comp_closure {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) ⦃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_left {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {a b c : C} (f : a b) (g₁ g₂ : b c) :

theorem category_theory.quotient.comp_right {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {a b c : C} (g : b c) (f₁ f₂ : a b) :

def category_theory.quotient.hom {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) :

Hom-sets of the quotient category.

Equations
@[instance]
def category_theory.quotient.inhabited {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) (a : category_theory.quotient r) :

Equations
def category_theory.quotient.comp {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) ⦃a b c : category_theory.quotient r⦄ :

Composition in the quotient category.

Equations
@[simp]
theorem category_theory.quotient.comp_mk {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {a b c : category_theory.quotient r} (f : a.as b.as) (g : b.as c.as) :

def category_theory.quotient.functor {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) :

The functor from a category to its quotient.

Equations
@[simp]
theorem category_theory.quotient.functor_map {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) (_x _x_1 : C) (f : _x _x_1) :

@[simp]
theorem category_theory.quotient.functor_obj_as {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) (a : C) :

theorem category_theory.quotient.induction {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {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

theorem category_theory.quotient.sound {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {a b : C} {f₁ f₂ : a b} :

@[simp]
theorem category_theory.quotient.lift_map {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {D : Type u_1} [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} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {D : Type u_1} [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} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {D : Type u_1} [category_theory.category D] (F : C D) :
(∀ (x y : C) (f₁ f₂ : x y), r f₁ f₂F.map f₁ = F.map f₂)category_theory.quotient r D

The induced functor on the quotient category.

Equations
def category_theory.quotient.lift.is_lift {C : Type u} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {D : Type u_1} [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} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {D : Type u_1} [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} [category_theory.category C] (r : Π ⦃a b : C⦄, (a b)(a b) → Prop) {D : Type u_1} [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) :