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
Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.star_map_down_down (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C} (x✝ : X✝ ⟶ Y✝) :
    ⋯ = ⋯
    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
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.punitExt_hom_app_down_down {C : Type u} [Category.{v, u} C] (F G : Functor C (Discrete PUnit.{w + 1})) (X : C) :
      ⋯ = ⋯
      source
      @[simp]
      theorem CategoryTheory.Functor.punitExt_inv_app_down_down {C : Type u} [Category.{v, u} C] (F G : Functor C (Discrete PUnit.{w + 1})) (X : C) :
      ⋯ = ⋯
      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
      Instances For
        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.
        Instances For
          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_inverse {C : Type u} [Category.{v, u} C] :
          equiv.inverse = const (Discrete PUnit.{w + 1})
          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_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)