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) [CategoryTheory.Category.{v, u} C] :
∀ {X Y : C} (x : X Y), (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as) = (_ : { as := PUnit.unit }.as = { as := PUnit.unit }.as)

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

@[inline, reducible]

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

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Functor.equiv_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] :
    CategoryTheory.Functor.equiv.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.Iso.refl
    @[simp]
    theorem CategoryTheory.Functor.equiv_functor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} ) C) :
    CategoryTheory.Functor.equiv.functor.obj F = F.obj { as := PUnit.unit }
    @[simp]
    theorem CategoryTheory.Functor.equiv_functor_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
    ∀ {X Y : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} ) C} (θ : X Y), CategoryTheory.Functor.equiv.functor.map θ = θ.app { as := PUnit.unit }

    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

      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)