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'.
- 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
- category_theory.inhabited r = {default := {as := inhabited.default C _inst_2}}
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⦄ :
- intro : ∀ {C : Type u} [_inst_1 : category_theory.category C] (r : Π ⦃a b : C⦄, (a ⟶ b) → (a ⟶ b) → Prop) ⦃s t : C⦄ {a b : C} (f : s ⟶ a) (m₁ m₂ : a ⟶ b) (g : b ⟶ t), r m₁ m₂ → category_theory.quotient.comp_closure r (f ≫ m₁ ≫ g) (f ≫ m₂ ≫ g)
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) :
category_theory.quotient.comp_closure r g₁ g₂ → category_theory.quotient.comp_closure r (f ≫ g₁) (f ≫ g₂)
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) :
category_theory.quotient.comp_closure r f₁ f₂ → category_theory.quotient.comp_closure r (f₁ ≫ g) (f₂ ≫ g)
def
category_theory.quotient.hom
{C : Type u}
[category_theory.category C]
(r : Π ⦃a b : C⦄, (a ⟶ b) → (a ⟶ b) → Prop) :
category_theory.quotient r → category_theory.quotient r → Type v
Hom-sets of the quotient category.
Equations
- category_theory.quotient.hom r s t = quot (category_theory.quotient.comp_closure r)
@[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
- category_theory.quotient.inhabited r a = {default := quot.mk (category_theory.quotient.comp_closure r) (𝟙 a.as)}
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⦄ :
category_theory.quotient.hom r a b → category_theory.quotient.hom r b c → category_theory.quotient.hom r a c
Composition in the quotient category.
Equations
- category_theory.quotient.comp r = λ (hf : category_theory.quotient.hom r a b) (hg : category_theory.quotient.hom r b c), quot.lift_on hf (λ (f : a.as ⟶ b.as), quot.lift_on hg (λ (g : b.as ⟶ c.as), quot.mk (category_theory.quotient.comp_closure r) (f ≫ g)) _) _
@[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) :
category_theory.quotient.comp r (quot.mk (category_theory.quotient.comp_closure r) f) (quot.mk (category_theory.quotient.comp_closure r) g) = quot.mk (category_theory.quotient.comp_closure r) (f ≫ g)
@[instance]
def
category_theory.quotient.category
{C : Type u}
[category_theory.category C]
(r : Π ⦃a b : C⦄, (a ⟶ b) → (a ⟶ b) → Prop) :
Equations
- category_theory.quotient.category r = {to_category_struct := {to_has_hom := {hom := category_theory.quotient.hom r}, id := λ (a : category_theory.quotient r), quot.mk (category_theory.quotient.comp_closure r) (𝟙 a.as), comp := category_theory.quotient.comp r}, id_comp' := _, comp_id' := _, assoc' := _}
@[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) :
((category_theory.quotient.functor r).obj a).as = a
@[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) :
(category_theory.quotient.functor r).map f = quot.mk (category_theory.quotient.comp_closure r) f
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.
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} :
r f₁ f₂ → (category_theory.quotient.functor r).map f₁ = (category_theory.quotient.functor r).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) :
(category_theory.quotient.lift r F H).obj a = F.obj a.as
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) :
The induced functor on the quotient category.
Equations
- category_theory.quotient.lift r F H = {obj := λ (a : category_theory.quotient r), F.obj a.as, map := λ (a b : category_theory.quotient r) (hf : a ⟶ b), quot.lift_on hf (λ (f : a.as ⟶ b.as), F.map f) _, map_id' := _, map_comp' := _}
@[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) _
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
- category_theory.quotient.lift.is_lift r F H = category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl ((category_theory.quotient.functor r ⋙ category_theory.quotient.lift r F H).obj X)) _
@[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) :