Mathlib.CategoryTheory.PUnit

CategoryTheory.Functor.star definition

: C ⥤ Discrete PUnit.{w + 1}

Full source

/-- The constant functor sending everything to `PUnit.star`. -/
@[simps!]
def star : C ⥤ Discrete PUnit.{w + 1} :=
  (Functor.const _).obj ⟨⟨⟩⟩

Constant functor to the discrete singleton category

Informal description

The constant functor from a category $C$ to the discrete category on the singleton type `PUnit`, which sends every object and morphism in $C$ to the unique object `PUnit.star` and its identity morphism, respectively.

CategoryTheory.Functor.punitExt definition

(F G : C ⥤ Discrete PUnit.{w + 1}) : F ≅ G

Full source

/-- Any two functors to `Discrete PUnit` are isomorphic. -/
@[simps!]
def punitExt (F G : C ⥤ Discrete PUnit.{w + 1}) : F ≅ G :=
  NatIso.ofComponents fun X => eqToIso (by simp only [eq_iff_true_of_subsingleton])

Natural isomorphism between functors to the discrete singleton category

Informal description

For any two functors $F, G : C \to \text{Discrete PUnit}$ from a category $C$ to the discrete category on the singleton type $\text{PUnit}$, there exists a natural isomorphism between $F$ and $G$. This isomorphism is constructed by using the fact that all objects in $\text{Discrete PUnit}$ are equal (since it is a subsingleton), and thus the components of the natural isomorphism are given by the isomorphism induced by this equality.

CategoryTheory.Functor.punit_ext' theorem

(F G : C ⥤ Discrete PUnit.{w + 1}) : F = G

Full source

/-- Any two functors to `Discrete PUnit` are *equal*.
You probably want to use `punitExt` instead of this. -/
theorem punit_ext' (F G : C ⥤ Discrete PUnit.{w + 1}) : F = G :=
  Functor.ext fun X => by simp only [eq_iff_true_of_subsingleton]

Uniqueness of Functors to Singleton Category

Informal description

For any two functors $F, G : C \to \text{Discrete PUnit}$ from a category $C$ to the discrete category on the singleton type $\text{PUnit}$, we have $F = G$.

CategoryTheory.Functor.fromPUnit abbrev

(X : C) : Discrete PUnit.{w + 1} ⥤ C

Full source

/-- The functor from `Discrete PUnit` sending everything to the given object. -/
abbrev fromPUnit (X : C) : DiscreteDiscrete PUnit.{w + 1} ⥤ C :=
  (Functor.const _).obj X

Functor from Singleton Category to $C$ Sending Everything to $X$

Informal description

Given an object $X$ in a category $C$, the functor $\text{fromPUnit}(X)$ maps every object in the discrete category on the singleton type $\text{PUnit}$ to $X$, and every morphism to the identity morphism on $X$.

CategoryTheory.Functor.equiv definition

: Discrete PUnit.{w + 1} ⥤ C ≌ C

Full source

/-- Functors from `Discrete PUnit` are equivalent to the category itself. -/
@[simps]
def equiv : DiscreteDiscrete PUnit.{w + 1} ⥤ CDiscrete PUnit.{w + 1} ⥤ C ≌ C where
  functor :=
    { obj := fun F => F.obj ⟨⟨⟩⟩
      map := fun θ => θ.app ⟨⟨⟩⟩ }
  inverse := Functor.const _
  unitIso := NatIso.ofComponents fun _ => Discrete.natIso fun _ => Iso.refl _
  counitIso := NatIso.ofComponents Iso.refl

Equivalence between functors from $\text{Discrete PUnit}$ and $\mathcal{C}$

Informal description

The category of functors from the discrete category on the singleton type $\text{PUnit}$ to a category $\mathcal{C}$ is equivalent to $\mathcal{C}$ itself. The equivalence is given by: - The functor that evaluates a functor $F \colon \text{Discrete PUnit} \to \mathcal{C}$ at the unique object $\star$ of $\text{Discrete PUnit}$. - The inverse functor that sends an object $X \in \mathcal{C}$ to the constant functor $\text{const}(X) \colon \text{Discrete PUnit} \to \mathcal{C}$. - The unit and counit natural isomorphisms are given by the identity isomorphisms.

CategoryTheory.equiv_punit_iff_unique theorem

: Nonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ x y : C, Nonempty <| Unique (x ⟶ y)

Full source

/-- 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`) -/
theorem equiv_punit_iff_unique :
    NonemptyNonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ x y : C, Nonempty <| Unique (x ⟶ y) := by
  constructor
  · rintro ⟨h⟩
    refine ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩
    let f : x ⟶ y := by
      have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
      have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
      exact hx ≫ hy
    suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f
    have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y := by
      intro z
      simp [congrArg (· ≫ h.unitInv.app y) (h.unit.naturality z)]
    apply Subsingleton.intro
    intro a b
    rw [this a, this b]
    simp only [Functor.comp_map]
    congr 3
    apply ULift.ext
    simp [eq_iff_true_of_subsingleton]
  · rintro ⟨⟨p⟩, h⟩
    haveI := fun x y => (h x y).some
    refine
      Nonempty.intro
        (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩)
          ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.punitExt))
    exact
      NatIso.ofComponents fun _ =>
        { hom := default
          inv := default }

Equivalence to Singleton Category iff Unique Morphisms

Informal description

A category $C$ is equivalent to the discrete category on the singleton type $\text{PUnit}$ if and only if $C$ is nonempty and for every pair of objects $x, y$ in $C$, there exists a unique morphism from $x$ to $y$.