# Documentation

Mathlib.CategoryTheory.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.

@[simp]
theorem CategoryTheory.Functor.star_map_down_down (C : Type u) :
∀ {X Y : C} (x : X Y), (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as) = (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as)
@[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.

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

Any two functors to Discrete PUnit are isomorphic.

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.

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

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

Instances For
@[simp]
theorem CategoryTheory.Functor.equiv_counitIso {C : Type u} :
CategoryTheory.Functor.equiv.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.Iso.refl
@[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_unitIso {C : Type u} :
CategoryTheory.Functor.equiv.unitIso = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Discrete.natIso fun i => CategoryTheory.Iso.refl ((().obj X).obj i)
@[simp]
theorem CategoryTheory.Functor.equiv_inverse {C : Type u} :
CategoryTheory.Functor.equiv.inverse =
@[simp]
theorem CategoryTheory.Functor.equiv_functor_map {C : Type u} :
∀ {X Y : } (θ : X Y), CategoryTheory.Functor.equiv.functor.map θ = θ.app { as := PUnit.unit }

Functors from Discrete PUnit are equivalent to the category itself.

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)