# 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.

@[simp]
theorem CategoryTheory.Functor.star_map_down_down (C : Type u) :
∀ {X Y : C} (x : X Y), =
@[simp]
theorem CategoryTheory.Functor.star_obj_as (C : Type u) :
∀ (x : C), (.obj x).as = PUnit.unit

The constant functor sending everything to PUnit.star.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.punitExt_inv_app_down_down {C : Type u} (F : ) (G : ) (X : C) :
=
@[simp]
theorem CategoryTheory.Functor.punitExt_hom_app_down_down {C : Type u} (F : ) (G : ) (X : C) :
=
def CategoryTheory.Functor.punitExt {C : Type u} (F : ) (G : ) :
F G

Any two functors to Discrete PUnit are isomorphic.

Equations
Instances For
theorem CategoryTheory.Functor.punit_ext' {C : Type u} (F : ) (G : ) :
F = G

Any two functors to Discrete PUnit are equal. You probably want to use punitExt instead of this.

@[reducible, inline]
abbrev CategoryTheory.Functor.fromPUnit {C : Type u} (X : C) :

The functor from Discrete PUnit sending everything to the given object.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.equiv_functor_map {C : Type u} :
∀ {X Y : } (θ : X Y), CategoryTheory.Functor.equiv.functor.map θ = θ.app { as := PUnit.unit }
@[simp]
theorem CategoryTheory.Functor.equiv_functor_obj {C : Type u} (F : ) :
CategoryTheory.Functor.equiv.functor.obj F = F.obj { as := PUnit.unit }
@[simp]
theorem CategoryTheory.Functor.equiv_inverse {C : Type u} :
CategoryTheory.Functor.equiv.inverse =
@[simp]
theorem CategoryTheory.Functor.equiv_counitIso {C : Type u} :
CategoryTheory.Functor.equiv.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.Iso.refl
@[simp]
theorem CategoryTheory.Functor.equiv_unitIso {C : Type u} :
CategoryTheory.Functor.equiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : ) => CategoryTheory.Discrete.natIso fun (i : ) => CategoryTheory.Iso.refl (( X).obj i))

Functors from Discrete PUnit are equivalent to the category itself.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.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 CategoryTheory.Groupoid.ofHomUnique)