A type synonym for promoting any type to a category, with the only morphisms being equalities.
Equations
@[instance]
Equations
- category_theory.discrete_category α = {to_category_struct := {to_has_hom := {hom := λ (X Y : category_theory.discrete α), ulift (plift (X = Y))}, id := λ (X : category_theory.discrete α), {down := {down := _}}, comp := λ (X Y Z : category_theory.discrete α) (g : X ⟶ Y) (f : Y ⟶ Z), ulift.cases_on f (λ (f : plift (Y = Z)), f.cases_on (λ (f : Y = Z), eq.rec g f))}, id_comp' := _, comp_id' := _, assoc' := _}
@[instance]
Equations
- category_theory.discrete.inhabited = id _inst_1
@[simp]
def
category_theory.discrete.functor
{C : Type u₂}
[category_theory.category C]
{I : Type u₁} :
(I → C) → category_theory.discrete I ⥤ C
Any function I → C gives a functor discrete I ⥤ C.
Equations
@[simp]
theorem
category_theory.discrete.functor_obj
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
(F : I → C)
(i : I) :
(category_theory.discrete.functor F).obj i = F i
theorem
category_theory.discrete.functor_map
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
(F : I → C)
{i : category_theory.discrete I}
(f : i ⟶ i) :
(category_theory.discrete.functor F).map f = 𝟙 (F i)
def
category_theory.discrete.nat_trans
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
{F G : category_theory.discrete I ⥤ C} :
(Π (i : category_theory.discrete I), F.obj i ⟶ G.obj i) → (F ⟶ G)
For functors out of a discrete category, a natural transformation is just a collection of maps, as the naturality squares are trivial.
Equations
- category_theory.discrete.nat_trans f = {app := f, naturality' := _}
@[simp]
theorem
category_theory.discrete.nat_trans_app
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
{F G : category_theory.discrete I ⥤ C}
(f : Π (i : category_theory.discrete I), F.obj i ⟶ G.obj i)
(i : category_theory.discrete I) :
(category_theory.discrete.nat_trans f).app i = f i
def
category_theory.discrete.nat_iso
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
{F G : category_theory.discrete I ⥤ C} :
(Π (i : category_theory.discrete I), F.obj i ≅ G.obj i) → (F ≅ G)
For functors out of a discrete category, a natural isomorphism is just a collection of isomorphisms, as the naturality squares are trivial.
Equations
@[simp]
theorem
category_theory.discrete.nat_iso_hom_app
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
{F G : category_theory.discrete I ⥤ C}
(f : Π (i : category_theory.discrete I), F.obj i ≅ G.obj i)
(i : I) :
(category_theory.discrete.nat_iso f).hom.app i = (f i).hom
@[simp]
theorem
category_theory.discrete.nat_iso_inv_app
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
{F G : category_theory.discrete I ⥤ C}
(f : Π (i : category_theory.discrete I), F.obj i ≅ G.obj i)
(i : I) :
(category_theory.discrete.nat_iso f).inv.app i = (f i).inv
@[simp]
theorem
category_theory.discrete.nat_iso_app
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
{F G : category_theory.discrete I ⥤ C}
(f : Π (i : category_theory.discrete I), F.obj i ≅ G.obj i)
(i : I) :
(category_theory.discrete.nat_iso f).app i = f i
def
category_theory.discrete.nat_iso_functor
{C : Type u₂}
[category_theory.category C]
{I : Type u₁}
{F : category_theory.discrete I ⥤ C} :
Every functor F from a discrete category is naturally isomorphic (actually, equal) to
discrete.functor (F.obj).
Equations
@[simp]
@[simp]
def
category_theory.discrete.equivalence
{I J : Type u₁} :
I ≃ J → (category_theory.discrete I ≌ category_theory.discrete J)
We can promote a type-level equiv to
an equivalence between the corresponding discrete categories.
Equations
- category_theory.discrete.equivalence e = {functor := category_theory.discrete.functor ⇑e, inverse := category_theory.discrete.functor ⇑(e.symm), unit_iso := category_theory.discrete.nat_iso (λ (i : category_theory.discrete I), category_theory.eq_to_iso _), counit_iso := category_theory.discrete.nat_iso (λ (j : category_theory.discrete J), category_theory.eq_to_iso _), functor_unit_iso_comp' := _}
@[simp]
@[simp]
def
category_theory.discrete.equiv_of_equivalence
{α β : Type u₁} :
(category_theory.discrete α ≌ category_theory.discrete β) → α ≃ β
We can convert an equivalence of discrete categories to a type-level equiv.
@[simp]
theorem
category_theory.discrete.equiv_of_equivalence_inv_fun
{α β : Type u₁}
(h : category_theory.discrete α ≌ category_theory.discrete β)
(a : category_theory.discrete β) :
@[simp]
theorem
category_theory.discrete.equiv_of_equivalence_to_fun
{α β : Type u₁}
(h : category_theory.discrete α ≌ category_theory.discrete β)
(a : category_theory.discrete α) :
A discrete category is equivalent to its opposite category.
Equations
- category_theory.discrete.opposite α = let F : category_theory.discrete α ⥤ (category_theory.discrete α)ᵒᵖ := category_theory.discrete.functor (λ (x : α), opposite.op x) in category_theory.equivalence.mk F.left_op F (category_theory.nat_iso.of_components (λ (X : (category_theory.discrete α)ᵒᵖ), _.mpr (category_theory.iso.refl X)) _) (category_theory.discrete.nat_iso (λ (X : category_theory.discrete α), _.mpr (category_theory.iso.refl X)))
@[simp]
theorem
category_theory.discrete.functor_map_id
{J : Type v₁}
{C : Type u₂}
[category_theory.category C]
(F : category_theory.discrete J ⥤ C)
{j : category_theory.discrete J}
(f : j ⟶ j) :