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
.
@[simp]
@[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
The constant functor sending everything to PUnit.star
.
Equations
- CategoryTheory.Functor.star C = (CategoryTheory.Functor.const C).obj { as := PUnit.unit }
Instances For
@[simp]
theorem
CategoryTheory.Functor.punitExt_hom_app_down_down
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} ))
(G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} ))
(X : C)
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.Functor.punitExt_inv_app_down_down
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} ))
(G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} ))
(X : C)
:
⋯ = ⋯
def
CategoryTheory.Functor.punitExt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} ))
(G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} ))
:
F ≅ G
Any two functors to Discrete PUnit
are isomorphic.
Equations
- F.punitExt G = CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.eqToIso ⋯) ⋯
Instances For
theorem
CategoryTheory.Functor.punit_ext'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} ))
(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.
@[reducible, inline]
The functor from Discrete PUnit
sending everything to the given object.
Equations
Instances For
@[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 }
@[simp]
theorem
CategoryTheory.Functor.equiv_counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
:
CategoryTheory.Functor.equiv.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.Iso.refl ⋯
@[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} )
@[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 (i : CategoryTheory.Discrete PUnit.{w + 1} ) =>
CategoryTheory.Iso.refl
(((CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} ) C)).obj X).obj
i))
⋯
@[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 }
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
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
)