HepLean 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) [CategoryTheory.Category.{v, u} C] :
CategoryTheory.Functor C (CategoryTheory.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) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (x✝ : X✝ ⟶ Y✝) :
    ⋯ = ⋯
    source
    @[simp]
    theorem CategoryTheory.Functor.star_obj_as (C : Type u) [CategoryTheory.Category.{v, u} C] (x✝ : C) :
    ((CategoryTheory.Functor.star C).obj x✝).as = PUnit.unit
    source
    def CategoryTheory.Functor.punitExt {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} )) (X : C) :
      ⋯ = ⋯
      source
      @[simp]
      theorem CategoryTheory.Functor.punitExt_inv_app_down_down {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} )) (X : C) :
      ⋯ = ⋯
      source
      theorem CategoryTheory.Functor.punit_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (X : C) :
      CategoryTheory.Functor (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] :
        CategoryTheory.Functor (CategoryTheory.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} [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 }
          source
          @[simp]
          theorem CategoryTheory.Functor.equiv_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] :
          CategoryTheory.Functor.equiv.inverse = CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{w + 1} )
          source
          @[simp]
          theorem CategoryTheory.Functor.equiv_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] :
          CategoryTheory.Functor.equiv.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.Iso.refl ⋯
          source
          @[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 }
          source
          @[simp]
          theorem CategoryTheory.Functor.equiv_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] :
          CategoryTheory.Functor.equiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} ) C) => CategoryTheory.Discrete.natIso fun (x_1 : CategoryTheory.Discrete PUnit.{w + 1} ) => CategoryTheory.Iso.refl (((CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} ) C)).obj x).obj x_1)) ⋯
          source
          theorem CategoryTheory.equiv_punit_iff_unique (C : Type u) [CategoryTheory.Category.{v, u} C] :
          Nonempty (C ≌ CategoryTheory.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)