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_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
          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
                Instances For
                  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_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_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)