# mathlibdocumentation

category_theory.punit

# The category discrete punit#

We define star : C ⥤ discrete punit sending everything to punit.star, show that any two functors to discrete punit are naturally isomorphic, and construct the equivalence (discrete punit ⥤ C) ≌ C.

def category_theory.functor.star (C : Type u)  :

The constant functor sending everything to punit.star.

Equations
• = {as := punit.star}
@[simp]
theorem category_theory.functor.star_map_down_down (C : Type u) (j j' : C) (f : j j') :
_ = _
@[simp]
theorem category_theory.functor.punit_ext_inv_app {C : Type u} (F G : C ) (X : C) :
(F.punit_ext G).inv.app X =
@[simp]
theorem category_theory.functor.punit_ext_hom_app {C : Type u} (F G : C ) (X : C) :
(F.punit_ext G).hom.app X =
def category_theory.functor.punit_ext {C : Type u} (F G : C ) :
F G

Any two functors to discrete punit are isomorphic.

Equations
theorem category_theory.functor.punit_ext' {C : Type u} (F G : C ) :
F = G

Any two functors to discrete punit are equal. You probably want to use punit_ext instead of this.

@[reducible]
def category_theory.functor.from_punit {C : Type u} (X : C) :

The functor from discrete punit sending everything to the given object.

@[simp]
@[simp]
theorem category_theory.functor.equiv_unit_iso {C : Type u}  :
category_theory.functor.equiv.unit_iso = category_theory.nat_iso.of_components (λ (X : , category_theory.discrete.nat_iso (λ (i : , i.cases_on (λ (i : punit), i.cases_on (category_theory.iso.refl (((𝟭 .obj X).obj {as := punit.star}))))) category_theory.functor.equiv._proof_3
@[simp]
theorem category_theory.functor.equiv_functor_map {C : Type u} (F G : C) (θ : F G) :
= θ.app {as := punit.star}
@[simp]
theorem category_theory.functor.equiv_counit_iso {C : Type u}  :
category_theory.functor.equiv.counit_iso = category_theory.functor.equiv._proof_4
def category_theory.functor.equiv {C : Type u}  :

Functors from discrete punit are equivalent to the category itself.

Equations
@[simp]
theorem category_theory.functor.equiv_functor_obj {C : Type u}  :
= F.obj {as := punit.star}
theorem category_theory.equiv_punit_iff_unique (C : Type u)  :
∀ (x y : C), nonempty (unique (x y))

A category being equivalent to punit is equivalent to it having a unique morphism between any two objects. (In fact, such a category is also a groupoid; see groupoid.of_hom_unique)