Quotient category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[class]
structure
category_theory.congruence
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C) :
Prop
- is_equiv : ∀ {X Y : C}, is_equiv (X ⟶ Y) r
- comp_left : ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, r g g' → r (f ≫ g) (f ≫ g')
- comp_right : ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z), r f f' → r (f ≫ g) (f' ≫ g)
A hom_rel is a congruence when it's an equivalence on every hom-set, and it can be composed
from left and right.
Instances of this typeclass
theorem
category_theory.quotient.ext_iff
{C : Type u_1}
{_inst_1 : category_theory.category C}
{r : hom_rel C}
(x y : category_theory.quotient r) :
theorem
category_theory.quotient.ext
{C : Type u_1}
{_inst_1 : category_theory.category C}
{r : hom_rel C}
(x y : category_theory.quotient r)
(h : x.as = y.as) :
x = y
@[ext]
structure
category_theory.quotient
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C) :
Type u_1
- as : C
A type synonym for C, thought of as the objects of the quotient category.
Instances for category_theory.quotient
- category_theory.quotient.has_sizeof_inst
- category_theory.quotient.inhabited
- category_theory.quotient.category
@[protected, instance]
def
category_theory.quotient.inhabited
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
[inhabited C] :
Equations
- category_theory.quotient.inhabited r = {default := {as := inhabited.default _inst_2}}
inductive
category_theory.quotient.comp_closure
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
⦃s t : C⦄ :
- intro : ∀ {C : Type u_1} [_inst_1 : category_theory.category C] {r : hom_rel C} ⦃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_closure.of
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{a b : C}
(m₁ m₂ : a ⟶ b)
(h : r m₁ m₂) :
theorem
category_theory.quotient.comp_left
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{a b c : C}
(f : a ⟶ b)
(g₁ g₂ : b ⟶ c)
(h : 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_1}
[category_theory.category C]
(r : hom_rel C)
{a b c : C}
(g : b ⟶ c)
(f₁ f₂ : a ⟶ b)
(h : 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_1}
[category_theory.category C]
(r : hom_rel C)
(s t : category_theory.quotient r) :
Type u_2
Hom-sets of the quotient category.
Equations
- category_theory.quotient.hom r s t = quot (category_theory.quotient.comp_closure r)
Instances for category_theory.quotient.hom
@[protected, instance]
def
category_theory.quotient.hom.inhabited
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
(a : category_theory.quotient r) :
Equations
- category_theory.quotient.hom.inhabited r a = {default := quot.mk (category_theory.quotient.comp_closure r) (𝟙 a.as)}
def
category_theory.quotient.comp
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
⦃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_1}
[category_theory.category C]
(r : hom_rel C)
{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)
@[protected, instance]
Equations
- category_theory.quotient.category r = {to_category_struct := {to_quiver := {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' := _}
The functor from a category to its quotient.
Equations
Instances for category_theory.quotient.functor
@[simp]
theorem
category_theory.quotient.functor_map
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
(_x _x_1 : C)
(f : _x ⟶ _x_1) :
(category_theory.quotient.functor r).map f = quot.mk (category_theory.quotient.comp_closure r) f
@[simp]
theorem
category_theory.quotient.functor_obj_as
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
(a : C) :
((category_theory.quotient.functor r).obj a).as = a
@[protected, instance]
noncomputable
def
category_theory.quotient.functor.category_theory.full
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C) :
Equations
- category_theory.quotient.functor.category_theory.full r = {preimage := λ (X Y : C) (f : (category_theory.quotient.functor r).obj X ⟶ (category_theory.quotient.functor r).obj Y), quot.out f, witness' := _}
@[protected, instance]
def
category_theory.quotient.functor.category_theory.ess_surj
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C) :
@[protected]
theorem
category_theory.quotient.induction
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{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
@[protected]
theorem
category_theory.quotient.sound
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{a b : C}
{f₁ f₂ : a ⟶ b}
(h : r f₁ f₂) :
(category_theory.quotient.functor r).map f₁ = (category_theory.quotient.functor r).map f₂
theorem
category_theory.quotient.functor_map_eq_iff
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
[category_theory.congruence r]
{X Y : C}
(f f' : X ⟶ Y) :
(category_theory.quotient.functor r).map f = (category_theory.quotient.functor r).map f' ↔ r f f'
@[simp]
theorem
category_theory.quotient.lift_map
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[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_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[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_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[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 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' := _}
theorem
category_theory.quotient.lift_spec
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[category_theory.category D]
(F : C ⥤ D)
(H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) :
theorem
category_theory.quotient.lift_unique
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[category_theory.category D]
(F : C ⥤ D)
(H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂)
(Φ : category_theory.quotient r ⥤ D)
(hΦ : category_theory.quotient.functor r ⋙ Φ = F) :
Φ = category_theory.quotient.lift r F H
def
category_theory.quotient.lift.is_lift
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[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_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[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_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[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) :
theorem
category_theory.quotient.lift_map_functor_map
{C : Type u_1}
[category_theory.category C]
(r : hom_rel C)
{D : Type u_3}
[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 Y : C}
(f : X ⟶ Y) :
(category_theory.quotient.lift r F H).map ((category_theory.quotient.functor r).map f) = F.map f