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.

source
def CategoryTheory.Functor.star (C : Type u) [Category.{v, u} C] :
Functor C (Discrete PUnit.{w + 1})

The constant functor sending everything to PUnit.star.

Equations
source
@[simp]
theorem CategoryTheory.Functor.star_obj_as (C : Type u) [Category.{v, u} C] (x✝ : C) :
((star C).obj x✝).as = PUnit.unit
source
def CategoryTheory.Functor.punitExt {C : Type u} [Category.{v, u} C] (F G : Functor C (Discrete PUnit.{w + 1})) :
F ≅ G

Any two functors to Discrete PUnit are isomorphic.

Equations
source
theorem CategoryTheory.Functor.punit_ext' {C : Type u} [Category.{v, u} C] (F G : Functor C (Discrete PUnit.{w + 1})) :
F = G

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

source
@[reducible, inline]
abbrev CategoryTheory.Functor.fromPUnit {C : Type u} [Category.{v, u} C] (X : C) :
Functor (Discrete PUnit.{w + 1}) C

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

Equations
source
def CategoryTheory.Functor.equiv {C : Type u} [Category.{v, u} C] :
Functor (Discrete PUnit.{w + 1}) C ≌ C

Functors from Discrete PUnit are equivalent to the category itself.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Functor.equiv_functor_obj {C : Type u} [Category.{v, u} C] (F : Functor (Discrete PUnit.{w + 1}) C) :
equiv.functor.obj F = F.obj { as := PUnit.unit }
source
@[simp]
theorem CategoryTheory.Functor.equiv_counitIso {C : Type u} [Category.{v, u} C] :
equiv.counitIso = NatIso.ofComponents Iso.refl ⋯
source
@[simp]
theorem CategoryTheory.Functor.equiv_functor_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Functor (Discrete PUnit.{w + 1}) C} (θ : X✝ ⟶ Y✝) :
equiv.functor.map θ = θ.app { as := PUnit.unit }
source
@[simp]
theorem CategoryTheory.Functor.equiv_inverse {C : Type u} [Category.{v, u} C] :
equiv.inverse = const (Discrete PUnit.{w + 1})
source
@[simp]
theorem CategoryTheory.Functor.equiv_unitIso {C : Type u} [Category.{v, u} C] :
equiv.unitIso = NatIso.ofComponents (fun (x : Functor (Discrete PUnit.{w + 1}) C) => Discrete.natIso fun (x_1 : Discrete PUnit.{w + 1}) => Iso.refl (((Functor.id (Functor (Discrete PUnit.{w + 1}) C)).obj x).obj x_1)) ⋯
source
theorem CategoryTheory.equiv_punit_iff_unique (C : Type u) [Category.{v, u} C] :
Nonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ (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)